F*
Verktøy
Handlinger
Generelt
Skriv ut / eksporter
På andre prosjekter
Referanseløs: Denne artikkelen inneholder enliste over kilder, litteratur ellereksterne lenker, men enkeltopplysninger lar seg ikkeverifisere fordi det mangler konkrete kildehenvisninger i form av fotnotebasertereferanser. Du kan hjelpe til med å sjekke opplysningene mot kildemateriale og legge inn referanser. Opplysninger uten kildehenvisning i form av referanser kan bli fjernet. |
F* | |||
---|---|---|---|
![]() | |||
Paradigme | Multi-paradigme:Funksjonell programmering,imperativ programmering | ||
Utviklet av | Microsoft Research,INRIA | ||
Siste versjon(er) | 0.9.0, 0.9.1, 0.9.1.1, 0.9.4.0, 0.9.5.0, 0.9.6.0 | ||
Typetildeling | inferens, sterk, dependent typing, statisk, refinement typing | ||
OS | multiplattform | ||
Lisens | Apache License 2.0 | ||
Implementert i | |||
F Sharp | |||
Påvirket av | |||
F Sharp,Objective Caml,Standard ML,Dafny,Lean |
F*, også skrevetFstar, er etMetaLanguage-basert språk som er utviklet hosMicrosoft Research. F* er sterkt inspirert avF#, et funksjonelt programmeringsspråk også utviklet av Microsoft Research ved Cambridge. Språket er avhengig av eksisterende typer og egner seg spesielt til verifisering av kode som foretar seg distribuerte kalkulasjoner.
Følgende eksempel er kode skrevet i F*:
moduleHellotypezero=x:int{x=0}letfail=assert<0=1>()