| F* | |
|---|---|
| Jazyková třída |
multiparadigma : funkční , objektově orientovaný , zobecněný , imperativní programování |
| Autor | Microsoft Research a INRIA [1] |
| Vývojář | Microsoft Research [2] a INRIA |
| Uvolnění |
|
| Typový systém | přísné, statické, s odvozením typu , se závislými typy |
| Byl ovlivněn | Coq , Dafny , F# , Lean , OCaml , Standard ML |
| Licence | Licence na software Apache |
| webová stránka | fstar-lang.org |
| OS | Multiplatformní software ( Linux , macOS , Windows ) |
F * (vyslovuje se jako F star) je funkcionální programovací jazyk založený na ML a zaměřený na formální ověřování programů na něm vyvinutých.
Jeho typový systém zahrnuje závislé typy , monadické efekty a typy zpřesnění Tyto vyjadřovací prostředky jsou dostatečné pro přesné specifikace programů, včetně popisů funkční správnosti a bezpečnostních vlastností. Mechanismus kontroly typu v F* vám umožňuje prokázat, že programy odpovídají jejich specifikacím. To se provádí pomocí kombinace řešiče SMT a ručních nátisků . Programy napsané v F* lze přeložit do OCaml , F# a C pro další kompilaci a spuštění. Předchozí verze F* mohly být také přeloženy do JavaScriptu .
Nejnovější verze F* je napsána zcela ve společné podmnožině F* a F# a lze ji spustit pomocí OCaml nebo F#. Zdrojový kód jazyka je otevřen pod licencí Apache 2.0 a je aktivně vyvíjen na GitHubu [4] .
| Microsoft Research (MSR) | |||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Hlavní projekty |
| ||||||||||||||
| Laboratoře MSR |
| ||||||||||||||
| Kategorie | |||||||||||||||
| Bezplatný a otevřený software společnosti Microsoft | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| obecná informace |
| ||||||||||||
| Software _ |
| ||||||||||||
| licence | |||||||||||||
| související témata |
| ||||||||||||
| Kategorie | |||||||||||||