| F* | |
|---|---|
| Nyelvóra |
több paradigma : funkcionális , objektum-orientált , általánosított , kötelező programozás |
| Szerző | Microsoft Research és INRIA [1] |
| Fejlesztő | Microsoft Research [2] és INRIA |
| Kiadás | |
| Típusrendszer | szigorú, statikus, típuskövetkeztetéssel , függő típusokkal |
| Befolyásolt | Coq , Dafny , F# , Lean , OCaml , Standard ML |
| Engedély | Apache szoftverlicenc |
| Weboldal | fstar-lang.org |
| OS | Többplatformos szoftver ( Linux , macOS , Windows ) |
Az F * (ejtsd: F csillag) egy ML -alapú funkcionális programozási nyelv , amely az arra fejlesztett programok formális ellenőrzésére összpontosít .
Típusrendszere függő típusokat , monád effektusokat és finomítási típusokat tartalmaz Ezek a kifejező eszközök elegendőek a programok pontos specifikációihoz, beleértve a funkcionális helyesség és a biztonsági tulajdonságok leírását. Az F* típusellenőrző mechanizmusa lehetővé teszi annak bizonyítását, hogy a programok megfelelnek a specifikációiknak. Ez az SMT megoldó és a kézi bizonyítások kombinációjával történik . Az F* nyelven írt programok lefordíthatók OCaml , F# és C nyelvre a további fordítás és végrehajtás érdekében. Az F* korábbi verziói JavaScriptre is lefordíthatók .
Az F* legújabb verziója teljes egészében az F* és F# közös részhalmazában van írva, és OCaml vagy F# használatával futtatható. A nyelv forráskódja az Apache 2.0 licenc alatt nyílt, és aktívan fejlesztik a GitHubon [4] .
| Microsoft Research (MSR) | |||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Főbb projektek |
| ||||||||||||||
| MSR Labs |
| ||||||||||||||
| Kategória | |||||||||||||||
| Ingyenes és nyílt forráskódú Microsoft szoftver | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Általános információ |
| ||||||||||||
| Szoftver _ |
| ||||||||||||
| Licencek | |||||||||||||
| Kapcsolódó témák |
| ||||||||||||
| Kategória | |||||||||||||