Описание тега fstar

Описание тега Вопросы с тегом
F* (pronounced F star) is an ML-like functional programming language aimed at program verification.
1 ответ

Аппликативный функтор в F*: ошибка проверки типа

В качестве эксперимента, пытаясь познакомиться с F*, я попытался реализовать аппликативный функтор. Я застрял в странно выглядящей ошибке проверки типов. Я еще не уверен, связано ли это с какой-то функцией / логикой проверки типов, о которой я не зн…
08 авг '18 в 22:24
0 ответов

FStar - Различные результаты в режиме fstar и командной строке

Я следую учебному пособию для F * https://www.fstar-lang.org/tutorial/ и настроил Emacs с режимом fstar https://github.com/FStarLang/fstar-mode.el в Ubuntu. Я думаю, что я не понимаю, как правильно проверять типы файлов, потому что, когда я делаю эт…
01 янв '19 в 19:57
3 ответа

Как получить представление о запросе z3, когда не в Windows

На вики-странице https://github.com/FStarLang/FStar/wiki/Profiling-Z3-queries предлагается использовать Z3 Axiom Profiler; однако Z3 Axiom Profiler надежно работает только на Windows. Как я могу легко получить квантификаторы, которые стреляют больше…
21 янв '19 в 17:32
0 ответов

Используйте метапрограммирование на F* для синтаксической проверки аргумента функции

Я хотел бы написать функцию, которая обеспечивает, чтобы ее аргумент синтаксически был константной строкой. Вот что я попробовал: module Test module R = FStar.Reflection let is_literal (t: R.term) = match R.inspect_ln t with | R.Tv_Const (R.C_String…
05 фев '19 в 19:19
1 ответ

Использование нормализатора для уменьшения рекурсивной функции

Я хочу доказать свойство, параметризованное для конечного числа случаев. Я хотел бы разделить проблему на один экземпляр для каждого случая и решить каждый экземпляр отдельно. Вот пример, чтобы прояснить ситуацию: module Minimal open FStar.List open…
11 фев '19 в 18:47
1 ответ

Скомпилируйте проблему с FStar и моно

Я пытаюсь скомпилировать язык FStar на последних версиях Ubuntu и Mono. GitHub repo предоставляет некоторые инструкции по сборке, но у меня это не работает. После sudo apt-get install mono-complete fsharp mozroots --import --sync source setenv.sh ma…
12 авг '14 в 04:51
1 ответ

В чем разница между худой, f* и dafny?

Они из Microsoft и кажутся помощниками? Помимо синтаксических различий, есть ли практические аспекты, которые отличают их друг от друга (например, способность делать автоматизацию, выразительную силу и т. Д.)? Я новичок в формальной проверке. Редакт…
02 сен '17 в 05:57
0 ответов

Есть ли в F* функция поиска для проверки?

Как мы знаем, у нас есть "auto" (пробный поиск) в Agda (Ctrl+c Ctrl+a в Emacs), а также в Idris и Coq, но когда я копался в режиме Fma's Emacs, мне не удалось найти аналогичный функционал. Есть ли у F* эта функция? Если так, как я могу использовать …
10 авг '18 в 01:08
1 ответ

Предположим, что val и непрозрачные конструкции типа в F*

Я новичок в F*, и хотя учебник хорошо написан, мне не хватает хорошей страницы API для справки. Поэтому мне нужно точное значение для следующих конструкций: assume val name: type Я бы сказал, что эта строка записывается в решатель имя используется? …
02 апр '17 в 14:32
1 ответ

GDB с Emacs и F*

Я хотел бы отладить простую F* программу, используя Emacs fstar-mode и gdb. В самом конце вики режима fstar https://github.com/FStarLang/fstar-mode.el есть информация: The fstar-gdb command (M-x) attaches GDB to the current F* process and launches E…
21 янв '19 в 18:37
2 ответа

Как объявить ограничение hasEq?

Я только начинаю с F*, что означает, что я написал несколько строк вместе с учебником. Пока что это действительно интересно, и я бы хотел продолжить обучение. Первое, что я попытался сделать самостоятельно, - написать тип, представляющий непустой сп…
08 мар '17 в 16:08
1 ответ

Некоторые вопросы о самой слабой записи предварительных условий в руководстве F*

Глава 9 в руководстве F* имеет пример: b ::= x | true | false e ::= b | let x = e1 in e2 | assert b | if b then e1 else e2 WP b P = P b WP (let x = e1 in e2) P = WP e1 (fun x -> WP e2 P) WP (assert b) P = b /\ P b WP (if b then e1 else e2) P = (b…
11 фев '17 в 21:15
1 ответ

F* поддерживает линейные типы?

Согласно статье в Википедии о субструктурных системах типов, F* поддерживает некоторые типы линейных типов. Это правда? Если так, то как? Я не могу найти информацию об этом в руководстве по F *.
30 июл '18 в 20:04
0 ответов

Как доказать утверждения вида x. фи х в F*?

Я только начал изучать F*, изучая урок. Одно из упражнений - доказать, что reverse Функция в списках является инъективной. Поскольку это следует из того факта, что инволюции инъективны, я хотел бы выразить этот факт в виде леммы в F*. Для этого я оп…
29 дек '17 в 14:35
1 ответ

Начиная с Fstar

Я читал о F-звезде из некоторых статей и из учебника по F-звезде, но я совершенно заблудился, пытаясь понять его концепции. Например, зависимый тип, монады Дейкстры и т. Д. Что необходимо сделать, чтобы правильно понять и узнать о F-star? Любое объя…
09 сен '19 в 09:35
2 ответа

Предварительное условие не выполняется при вызове функции в другом модуле

Я пытаюсь вызвать функцию в другом модуле, который отвечает за сохранение предварительных и пост-условий в куче. В частности, он гарантирует, что переданная строка будет "читаемой" перед вызовом read: val readableFiles : ref fileList let readableFil…
18 ноя '19 в 06:21
1 ответ

Как проверить равенство двух FStar.Set's

Как проверить, равны ли два набора в FStar? Следующее выражение имеет типType0 не Tot Prims.boolпоэтому я не уверен, как использовать его, чтобы определить, равны ли наборы (например, в условном). Есть ли другая функция, которую следует использовать…
18 ноя '19 в 20:25
1 ответ

Взаимно индуктивные типы данных с параметрами типа

Я пытаюсь написать объявление двух взаимно индуктивных типов данных, которые оба принимают параметр типа в качестве аргументов следующим образом: noeq type foo 'a = | FooA: x: 'a -> foo 'a | Foob: y: bar 'a -> foo 'a and bar 'b = | BarA: x: in…
27 янв '20 в 19:17
1 ответ

Проблема с простым утверждением в FStar

Я только начал изучать FStar. Хочу отметить тот факт, что для каждого натурального числа существует большее число. let _ = assert (forall (m:nat). exists (n: nat). n > m) Это не удается, и я хотел бы знать, почему. Спасибо.
19 май '20 в 19:06
1 ответ

Странное поведение функции FStar

Кажется неправильным, чтобы следующая простая функция была принята как завершающая: val fnc : (nw: nat) -> (ni: nat) -> (ni_max: nat) -> bool let rec fnc nw ni ni_max = match ni with | ni_max -> false | _ -> fnc nw (nw + ni) ni_max Уд…
19 июн '20 в 18:41