| F* | |
|---|---|
| Kieliluokka |
moniparadigma : toiminnallinen , oliosuuntautunut , yleistetty , pakollinen ohjelmointi |
| Tekijä | Microsoft Research ja INRIA [1] |
| Kehittäjä | Microsoft Research [2] ja INRIA |
| Vapauta |
|
| Tyyppijärjestelmä | tiukka, staattinen, tyyppipäätelmillä , riippuvaisilla tyypeillä |
| Vaikutettu | Coq , Dafny , F# , Lean , OCaml , Standard ML |
| Lisenssi | Apache-ohjelmiston lisenssi |
| Verkkosivusto | fstar-lang.org |
| OS | Monialustaiset ohjelmistot ( Linux , macOS , Windows ) |
F * (lausutaan F star) on toiminnallinen ohjelmointikieli , joka perustuu ML :ään ja keskittyy sillä kehitettyjen ohjelmien muodolliseen todentamiseen .
Sen tyyppijärjestelmä sisältää riippuvaisia tyyppejä , monadisia efektejä ja tarkennustyyppejä Nämä ilmeikkäät keinot riittävät antamaan ohjelmille tarkkoja määritelmiä, mukaan lukien kuvaukset toiminnallisesta oikeellisuudesta ja suojausominaisuuksista. F*:n tyyppitarkistusmekanismin avulla voit todistaa, että ohjelmat ovat määritysten mukaisia. Tämä tehdään käyttämällä SMT-ratkaisijan ja manuaalisten todisteiden yhdistelmää . F*-kielellä kirjoitetut ohjelmat voidaan kääntää OCaml- , F# - ja C -kieleksi lisäkääntämistä ja suoritusta varten. F*:n aiemmat versiot voidaan myös kääntää JavaScriptiksi .
F*:n uusin versio on kirjoitettu kokonaan F*:n ja F#:n yhteiseen osajoukkoon, ja sitä voidaan käyttää joko OCaml- tai F#-komennolla. Kielen lähdekoodi on avoin Apache 2.0 -lisenssillä ja sitä kehitetään aktiivisesti GitHubissa [4] .
| Microsoft Research (MSR) | |||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Pääprojektit _ |
| ||||||||||||||
| MSR Labs |
| ||||||||||||||
| Kategoria | |||||||||||||||
| Ilmainen ja avoimen lähdekoodin Microsoft- ohjelmisto | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| yleistä tietoa |
| ||||||||||||
| Ohjelmisto_ _ |
| ||||||||||||
| Lisenssit | |||||||||||||
| liittyvät aiheet |
| ||||||||||||
| Kategoria | |||||||||||||