| F* | |
|---|---|
| Sprog klasse |
multi- paradigme : funktionel , objektorienteret , generaliseret , tvingende programmering |
| Forfatter | Microsoft Research og INRIA [1] |
| Udvikler | Microsoft Research [2] og INRIA |
| Frigøre | |
| Type system | streng, statisk, med typeslutning , med afhængige typer |
| Blev påvirket | Coq , Dafny , F# , Lean , OCaml , Standard ML |
| Licens | Apache-softwarelicens |
| Internet side | fstar-lang.org |
| OS | Cross-platform software ( Linux , macOS , Windows ) |
F * (udtales som F star) er et funktionelt programmeringssprog baseret på ML og fokuseret på den formelle verifikation af programmer udviklet på det.
Dets typesystem inkluderer afhængige typer , monadiske effekter og forfiningstyper Disse udtryksmidler er tilstrækkelige til at give præcise specifikationer for programmer, herunder beskrivelser af funktionel korrekthed og sikkerhedsegenskaber. Typekontrolmekanismen i F* giver dig mulighed for at bevise, at programmer er i overensstemmelse med deres specifikationer. Dette gøres ved hjælp af en kombination af SMT-løser og manuelle beviser . Programmer skrevet i F* kan oversættes til OCaml , F# og C for yderligere kompilering og eksekvering. Tidligere versioner af F* kunne også oversættes til JavaScript .
Den seneste version af F* er skrevet fuldstændigt i en fælles delmængde af F* og F# og kan køres ved hjælp af enten OCaml eller F#. Sprogets kildekode er åben under Apache 2.0 -licensen og er aktivt udviklet på GitHub [4] .
| Microsoft Research (MSR) | |||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Hovedprojekter _ |
| ||||||||||||||
| MSR Labs |
| ||||||||||||||
| Kategori | |||||||||||||||
| Gratis og open source Microsoft -software | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| generel information |
| ||||||||||||
| Software _ |
| ||||||||||||
| Licenser | |||||||||||||
| relaterede emner |
| ||||||||||||
| Kategori | |||||||||||||