https://wiki.dzmuh.com/index.php?action=history&feed=atom&title=F%2A 2026-05-07T02:53:36Z История изменений этой страницы в вики MediaWiki 1.38.4 https://wiki.dzmuh.com/index.php?title=F*&diff=11436&oldid=prev 2023-03-27T00:35:44Z

<p>Новая страница: «&#039;&#039;&#039;F *&#039;&#039;&#039; (произносится как F star) — <a href="/index.php?title=%D0%A4%D1%83%D0%BD%D0%BA%D1%86%D0%B8%D0%BE%D0%BD%D0%B0%D0%BB%D1%8C%D0%BD%D1%8B%D0%B9_%D1%8F%D0%B7%D1%8B%D0%BA_%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F&amp;action=edit&amp;redlink=1" class="new" title="Функциональный язык программирования (страница не существует)">функциональный язык программирования</a>, основанный на <a href="/index.php?title=ML&amp;action=edit&amp;redlink=1" class="new" title="ML (страница не существует)">ML</a> и ориентированный на <a href="/index.php?title=%D0%A4%D0%BE%D1%80%D0%BC%D0%B0%D0%BB%D1%8C%D0%BD%D0%B0%D1%8F_%D0%B2%D0%B5%D1%80%D0%B8%D1%84%D0%B8%D0%BA%D0%B0%D1%86%D0%B8%D1%8F_%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%BD%D0%BE%D0%B3%D0%BE_%D0%BE%D0%B1%D0%B5%D1%81%D0%BF%D0%B5%D1%87%D0%B5%D0%BD%D0%B8%D1%8F&amp;action=edit&amp;redlink=1" class="new" title="Формальная верификация программного обеспечения (страница не существует)">формальную верификацию</a> разрабатываемых на нём программ. Его система типов включает в с...»</p> <p><b>Новая страница</b></p><div>'''F *''' (произносится как F star) — [[функциональный язык программирования]], основанный на [[ML]] и ориентированный на [[Формальная верификация программного обеспечения|формальную верификацию]] разрабатываемых на нём программ.<br /> <br /> Его система типов включает в себя [[зависимые типы]], [[Монада (программирование)|монадические]] [[побочный эффект (программирование)|эффекты]] и {{Iw|типы-уточнения||en|Refinement type}}. Этих выразительных средств достаточно, чтобы задавать точные спецификации для программ, включая описания функциональной корректности и свойств безопасности. Механизм проверки типов в F* позволяет доказывать, что программы соответствуют их спецификациям. Это делается с использованием комбинации [[Задача выполнимости формул в теориях#SMT-решатели|SMT-решателя]] и [[Инструмент интерактивного доказательства теорем|ручных доказательств]]. Программы, написанные на F*, могут быть странслированы в [[OCaml]], [[F Sharp|F#]] и [[Си (язык программирования)|C]] для дальнейшей компиляции и выполнения. Предыдущие версии F* также можно было транслировать в [[JavaScript]].<br /> <br /> Последняя версия F* написана полностью на общем подмножестве F* и F# и может быть запущена как с использованием OCaml, так и с использованием F#. Исходный код языка открыт под лицензией [[Лицензия Apache|Apache 2.0]] и активно разрабатывается на [[GitHub]]&lt;ref&gt;{{cite web|url=https://github.com/FStarLang/FStar|title=FStarLang/FStar|website=GitHub|access-date=2020-05-28|archive-date=2020-07-10|archive-url=https://web.archive.org/web/20200710025302/https://github.com/FStarLang/FStar|deadlink=no}}&lt;/ref&gt;.<br /> <br /> == Примечания ==<br /> {{примечания}}<br /> <br /> == Ссылки ==<br /> {{википедия|F*}}<br /> * {{official|https://www.fstar-lang.org/}}<br /> * {{github|FStarLang|FStar}}<br /> <br /> [[Категория:Языки программирования по алфавиту]]<br /> [[Категория:Языки программирования, появившиеся в 2013 году]]<br /> [[Категория:Функциональные языки программирования]]<br /> [[Категория:Языки программирования семейства ML]]<br /> [[Категория:Языки программирования платформы .NET]]<br /> [[Категория:Microsoft Research]]<br /> [[Категория:Типозависимые формальные языки]]<br /> [[Категория:Автоматическое доказательство теорем]]</div>

Dzmuh