F* (dasturlash tili)
F* (F star deb talaffuz qilinadi) — dasturni tekshirishga qaratilgan funktsional dasturlash tilidir. Bu dasturlarning aniq spetsifikatsiyalarini, jumladan, funktsional toʻgʻriligi va xavfsizlik xususiyatlarini ifodalash imkonini beradi. F* turini tekshirgich SMT yechish va qoʻlda isbotlash kombinatsiyasidan foydalangan holda dasturlar oʻz spetsifikatsiyalariga mos kelishini isbotlashga qaratilgan. F* da yozilgan dasturlarni bajarish uchun OCaml, F# va C ga tarjima qilish mumkin. F* ning oldingi versiyalari JavaScriptga ham tarjima qilinishi mumkin edi.
Paradigmalari | Ko‘p paradigma: funsional, imperativ |
---|---|
Muallifi | Microsoft Research va Inria[1] |
Operatsion tizim | Linux, macOS, Windows |
Litsenziya | Apache License 2.0 |
Vebsayt | fstar-lang.org |
Bunga asos boʻlgan tillar | |
Coq, Dafny, F#, Lean, OCaml, Standard ML |
F* ning soʻnggi versiyasi toʻliq F* ning umumiy kichik toʻplamida va OCaml yuklash bloklarida yozilgan. Bu ochiq manba (Apache Litsenziyasi 2.0 ostida) va GitHubda faol ishlab chiqilmoqda[2].
Manbalar
tahrir- ↑ „Microsoft Research Inria Joint Centre“. MSR-INRIA.
- ↑ „FStarLang/FStar“. GitHub (2022-yil 31-oktyabr).
Adabiyotlar
tahrir- Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil (2017). "Dijkstra Monads for Free". 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. https://www.fstar-lang.org/papers/dm4free/.
- Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Forest, Simon; Bhargavan, Karthikeyan; Fournet, Cédric et al. (2016). "Dependent Types and Multi-Monadic Effects in F*". 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. https://www.fstar-lang.org/papers/mumon/.