diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 45d02dbaf..7b2c6af1f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -164,8 +164,8 @@ permissions: jobs: # ДИСЦИПЛИНА СЕМЕНИ идёт ПЕРВОЙ. Она читает `.flang` дерева и `bootstrap/*.c` - # планом на flang — 1087 файл; разбор в задаче 5821. - # СНЯТО 2026-10-02 файлов *.flang = 1087 + # планом на flang — 1097 файл; разбор в задаче 5821. + # СНЯТО 2026-10-02 файлов *.flang = 1097 # # Первой она стоит потому, что нарушение этого правила обесценивает ВСЕ # остальные работы разом. 24 августа 2026 имя типа «неотрицательное» ввели в diff --git a/docs/adr/0036-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md b/docs/adr/0036-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md index 40485c82b..3bc5d8412 100644 --- a/docs/adr/0036-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md +++ b/docs/adr/0036-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md @@ -192,7 +192,7 @@ flang check --proof --строго monoid.flang «Е не больше Е» не теорема, почему `0 × ∞` даёт не число, почему переставлять через скобки нельзя. Эти доводы не украшение: на них стоят посылки правил. - **Независимая проверяющая программа** — `flang/proof/checker/checker.c`, - 10257 строк. + 10395 строк. Она переигрывает записи и о новом виде значения не знает ничего. **И встречное число, которое меняет разговор о втором варианте.** Тип `целое` diff --git a/docs/adr/0050-a-reasoning-is-written-as-declared-words-and-fixed-sentences.md b/docs/adr/0050-a-reasoning-is-written-as-declared-words-and-fixed-sentences.md index 6ce430e7a..bbd406a30 100644 --- a/docs/adr/0050-a-reasoning-is-written-as-declared-words-and-fixed-sentences.md +++ b/docs/adr/0050-a-reasoning-is-written-as-declared-words-and-fixed-sentences.md @@ -57,30 +57,37 @@ | модус | программа | ядро, `check --proof --strict` | независимая проверяющая программа | |---|---|---|---| -| Barbara, единичная малая посылка (Сократ) | `socrates.flang` | доказано, код 0 | код 3, «не проверено» | -| Barbara | `barbara.flang` | доказано, код 0, один шаг `затем` | код 3 | -| Celarent | `celarent.flang` | доказано, код 0 | код 3 | -| Darii | `darii.flang` | доказано, код 0 | код 3 | -| Ferio | `ferio.flang` | доказано, код 0 | код 3 | +| Barbara, единичная малая посылка (Сократ) | `socrates.flang` | доказано, код 0 | код 0, «проверено» | +| Barbara | `barbara.flang` | доказано, код 0, один шаг `затем` | код 0 | +| Celarent | `celarent.flang` | доказано, код 0 | код 0 | +| Darii | `darii.flang` | доказано, код 0 | код 0 | +| Ferio | `ferio.flang` | доказано, код 0 | код 0 | | Camestres, прямая цель `(не x.P)` | `camestres.flang` | **отказ**, код 1: ядро не выводит отрицание | записи нет | -| Camestres, опровержением (`утверждаем нет`) | `camestres-by-refutation.flang` | доказано, код 0 | код 3 | +| Camestres, опровержением (`утверждаем нет`) | `camestres-by-refutation.flang` | доказано, код 0 | код 0 | | Barbara без промежуточного шага | `barbara-without-the-middle-step.flang` | **отказ**, код 1: ядро делает один модус поненс, не цепочку | записи нет | | подтверждение следствия | `affirming-the-consequent.flang` | отказ, код 1, `FLANG_PROOF_STEP` на строке заключения | записи нет | | нераспределённый средний | `undistributed-middle.flang` | отказ, код 1 | записи нет | | незаконное обращение | `illicit-conversion.flang` | отказ, код 1 | записи нет | | отрицание антецедента | `denying-the-antecedent.flang` | отказ, код 1 | записи нет | | экзистенциальный импорт (Barbari) | `existential-import.flang` | отказ, код 1 | записи нет | -| Darii через `есть такой … а именно` | `darii-with-the-existence-word.flang` | доказано, код 0 | **код 1, «не сошлось»** | -| посылки только в `таких что` | `socrates-with-premises-only-in-the-statement.flang` | доказано, код 0 | **код 1, «допущений в записи 0»** | -| посылки только в `дано` теоремы | `socrates-with-premises-only-in-the-theorem.flang` | **доказано, код 0 — дыра** (§5) | код 3 | +| Darii через `есть такой … а именно` | `darii-with-the-existence-word.flang` | доказано, код 0 | код 0 | +| посылки только в `таких что` | `socrates-with-premises-only-in-the-statement.flang` | доказано, код 0 | код 0 | +| посылки только в `дано` теоремы | `socrates-with-premises-only-in-the-theorem.flang` | **доказано, код 0 — дыра** (§5) | **код 1**: гипотеза не является допущением утверждения | | без теоремы, ядро само | `socrates-without-a-theorem.flang` | доказано, код 0 | код 3 | | предикаты — параметры-функции | `socrates-with-predicates-as-functions.flang` | доказано, код 0 | код 3 | Итог по вопросу (1): пять названных правильных модусов ядро доказывает, пять ошибок -отвергает кодом 1 с именем шага. Независимая проверяющая программа ни одного вывода из -допущений сегодня не переигрывает (шаг `по предположению` вне индукции — «на слове ядра», -код 3) — это её объявленная граница, а не расхождение; расхождения (код 1) ровно два, и оба -названы в таблице. +отвергает кодом 1 с именем шага. Независимая проверяющая программа переигрывает все пять +сама и отвечает кодом 0. Шаг `по предположению` в утверждении без функции она выводит из +частей его `таких что` (разобранных по `и притом`), а не из строк `дано`: промежуточный шаг +`затем Ф` и цель обязаны выводиться одним шагом — Ф есть посылка; есть посылка `если А то Ф +иначе да` при известном А; Ф — конъюнкция таких; цель `нет` при известных Х и `не Х`. Цель +`есть такой м, а именно Т, что У` читается как У с Т на месте м. Каждый шаг ещё и судится +таблицей истинности по признакам `«x».«поле»`: нашлось присвоение, при котором посылки верны, +а шаг ложен, — код 1 с этим присвоением; шаг верен, но не одним шагом, — код 3. Записи, +составленные для пяти ошибочных модусов, отвергаются кодом 1. Правило стоит 102 строки кода +`checker.c` (храповик `checker-code-lines`); пробы — семья +`flang/proof/checker/tests/families/assumption-replay/`. Полный перебор: 256 модусов четырёх фигур прогнаны текстами через переводчик (`flang/proof/probes/syllogism/sentences/`, план `Binary` на 256 порождённых текстах, ключ @@ -118,13 +125,12 @@ «Сократ».«смертен»`. То же с постусловием: функция тождества на `неотрицательное` с постусловием `результат больше 0` и теоремой с `дано н больше 0` — «доказано», код 0, а `flang run` на нуле печатает `FLANG_PROPERTY`. Ядро не сверяет гипотезы теоремы с -ограничениями утверждения. Независимая проверяющая программа спасает лишь тем, что не даёт -нуля (код 3). Задача — [5311](../tasks/5311-a-theorem-hypothesis-is-not-checked-against-the-statement.md). +ограничениями утверждения. Независимая проверяющая программа отвергает такую запись кодом 1: +гипотеза не является допущением утверждения. Задача — [5311](../tasks/5311-a-theorem-hypothesis-is-not-checked-against-the-statement.md). Следствие для этого решения: переводчик пишет посылки **в `таких что` утверждения** — тогда утверждение само говорит, при каких допущениях доказано заключение, — и повторяет их в `дано`, -потому что без строк `дано` независимая проверяющая программа отвечает кодом 1 (запись не -несёт допущений из `таких что`). +чтобы теорема читалась сама по себе; проверяющей программе хватает `таких что`. ## 6. Словарь и образцы предложений @@ -178,9 +184,9 @@ * **Посылки отдельными `утверждение` и шаг `по свойству`** (`programs/conditional.flang`): честно, но файл уходит кодом 3 «доказано ПРИ УСЛОВИИ» — посылка сама «объявлено, не доказано». Силлогизм — это «из посылок следует», а не «посылки верны». -* **Цель через `есть такой … а именно`** для частного заключения: ядро доказывает, а - независимая проверяющая программа отвечает кодом 1. Заключение пишется конъюнкцией о - свидетеле. +* **Цель через `есть такой … а именно`** для частного заключения: ядро доказывает, и + проверяющая программа переигрывает, но конъюнкция о свидетеле короче и читается прямо. + Заключение пишется ею. ## 8. Цена в грамматике, если делать словом языка @@ -211,8 +217,6 @@ прямой целью, без опровержения. * **Цепочка охран:** повторять модус поненс до неподвижной точки, чтобы `затем` не требовался на каждое звено. Дёшево: перебор конечен. -* **Проверяющая программа переигрывает `по предположению` вне индукции** и читает допущения - из `таких что` утверждения — иначе силлогизм навсегда «на слове ядра». * Если рассуждение становится файлом языка: вид файла `.рассуждение` со своим разбором (§6), разворачивающимся в `объект` + `утверждение` + `следует` ровно так, как печатает `--plan Translate`; отказ разбора называет слово и предложение. diff --git a/docs/course/README.md b/docs/course/README.md index 7e9abca61..bcca865cf 100644 --- a/docs/course/README.md +++ b/docs/course/README.md @@ -172,7 +172,7 @@ docs/course/check.flang: проверено — разбор, типы, заве | ответы девяти целей | сборка и запуск девяти напечатанных программ настоящими тулчейнами этой машины: `cc`/`g++` 15.2.0, go 1.26.5, rustc 1.97.1, javac 26-internal, Elixir 1.20.3 на Erlang/OTP 29, node 26.7.0, Python 3.14.4, .NET 10.0.110 | | 82 задачи LeetCode, десятка самых коротких | `ls`, `wc -l`, счёт строк `пример` | | 53 файлов и 32 526 строки библиотеки | `ls flang/stdlib/*.flang`, `cat … \| wc -l` | -| 726 заметки, 242 примеров, 413 файл доказательств | `ls`, `find` | +| 726 заметки, 242 примеров, 423 файл доказательств | `ls`, `find` | | 2 из 20 — цена доказательств | `docs/benchmark-proof-cost-2.md`, замер 16 августа | **Чего переснять не удалось, и это надо знать.** diff --git a/docs/design/nositel-tochnogo-celogo.md b/docs/design/nositel-tochnogo-celogo.md index 5f2278674..eaba62348 100644 --- a/docs/design/nositel-tochnogo-celogo.md +++ b/docs/design/nositel-tochnogo-celogo.md @@ -441,7 +441,7 @@ flang check n-zapis-v-chislo.flang первая правка, и назвать её сейчас, не написав, значило бы выдумать. 2. **Цену принуждения канона.** Сколько стоит запретить литерал-список в позиции нового типа — не мерил: это решение задачи 1412, а не замер. -3. **Цену для проверяющей программы.** `checker.c` (10257 строк) +3. **Цену для проверяющей программы.** `checker.c` (10395 строк) о новом типе не знает ничего, и бюджет ему ADR-0035 §7 оценил в +150…+250 строк кода по образцу ADR-0029. Это оценка, и моя записка её не улучшает. 4. **Скорость того же в рантайме.** Все числа §5 — арифметика, написанная НА ЯЗЫКЕ. diff --git a/docs/flang/proof/checker/README.md b/docs/flang/proof/checker/README.md index af5d1a4d3..4cf50ebd9 100644 --- a/docs/flang/proof/checker/README.md +++ b/docs/flang/proof/checker/README.md @@ -174,6 +174,20 @@ bootstrap/flang run-script trust:ceiling что тело функции: литерал, `длина`, сумма, произведение на положительный литерал. Неотрицательным по объявлению считается только имя, связанное `для всех` типом-отрезком (`неотрицательное`); ограничение `таких что` дна не даёт. +22. **Шаг `по предположению` в утверждении без функции выводится из его посылок.** + Когда все шаги теоремы обоснованы `по предположению`, нет ни индукции, ни + случаев, а каждое высказывание собрано из признаков `«x».«поле»` (`x` + связан `для всех`, поле объявлено `признак` в `объект` его типа), посылками + служат части `таких что` утверждения, разобранные по `и притом`, — строки + `дано` теоремы в вывод не идут. Промежуточный шаг `затем Ф по предположению` + и цель обязаны выводиться одним шагом из посылок и выведенного раньше: Ф + есть посылка; есть посылка `если А то Ф иначе да` при известном А; Ф — + конъюнкция таких; цель `нет` при известных Х и `не Х`. Цель `есть такой м, + а именно Т, что У` сличается с обещанной и выводится как У с Т на месте м. + Каждый шаг ещё и судится таблицей истинности по признакам: нашлось + присвоение, при котором посылки верны, а шаг ложен, — «НЕ СОШЛОСЬ» с этим + присвоением; шаг верен, но не одним шагом, — место остаётся на слове ядра. + Пробы — `tests/families/assumption-replay/`. Сверх того: **ни одной непрочитанной строки**. Строка записи, вид которой чекеру не известен, — отказ, а не «ладно». Мутационная проба (3000 порченых diff --git a/docs/four-coverages.md b/docs/four-coverages.md index 802ca424e..f06b34448 100644 --- a/docs/four-coverages.md +++ b/docs/four-coverages.md @@ -25,8 +25,8 @@ bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 90000 **Что меряет.** Долю мест в СОБСТВЕННЫХ записях доказательства компилятора, которые независимый проверяющий на C ([`flang/proof/checker/checker.c`](../flang/proof/checker/checker.c)) переиграл сам, а не принял на слово у ядра. Записи лежат готовыми в -`flang/proof/checker/tests/records/corpus/` — по одной на программу-образец, всего 91. - +`flang/proof/checker/tests/records/corpus/` — по одной на программу-образец, всего 93. + Снимается: `bootstrap/flang io flang/proof/replay-share.fscript`. **Что это даёт сказать.** Что у этого набора записей слово «доказано» в отчёте компилятора не diff --git a/docs/site/index.md b/docs/site/index.md index c5c545306..60f30f629 100644 --- a/docs/site/index.md +++ b/docs/site/index.md @@ -143,7 +143,7 @@ recounted on every push by `sh scripts/guards/published-vs-tree.sh --числа` steps: `дано` (given), `утверждаем` (we claim), `затем … по свойству «…»` (then … by property …), `индукция по …` (induction on …), `следовательно доказано` (hence proved). It reads like a proof in Isabelle's Isar, not like a script of -tactics. There are **303** such theorems in the repository, 55 of them in the +tactics. There are **308** such theorems in the repository, 55 of them in the standard library (`grep -rac '^\s*теорема ' flang --include='*.flang'`, summed with `awk`). diff --git a/docs/site/index.ru.md b/docs/site/index.ru.md index 6ac1ea0df..b549a62b1 100644 --- a/docs/site/index.ru.md +++ b/docs/site/index.ru.md @@ -141,7 +141,7 @@ bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000 **Доказательство руками можно писать и здесь.** `теорема` пишется по шагам: `дано`, `утверждаем`, `затем … по свойству «…»`, `индукция по …`, `следовательно доказано`. Это читается как доказательство на Isar из Isabelle, а -не как скрипт из тактик. Таких теорем в дереве языка **303**, из них **55** в +не как скрипт из тактик. Таких теорем в дереве языка **308**, из них **55** в стандартной библиотеке (`grep -rac '^\s*теорема ' flang --include='*.flang'`, сумма по `awk`). diff --git a/docs/site/proofs.md b/docs/site/proofs.md index c23f62138..c6cd42072 100644 --- a/docs/site/proofs.md +++ b/docs/site/proofs.md @@ -66,7 +66,7 @@ proof by hand**, as in Coq or Isabelle. A `теорема` (theorem) is written steps: `дано` (given), `утверждаем` (we claim), `затем … по свойству «…»` (then … by property …), `индукция по …` (induction on …), `следовательно доказано` (hence proved). It reads like Isar in Isabelle, and the prover checks each step; -it searches for nothing. There are 303 such theorems in the repository, 55 of +it searches for nothing. There are 308 such theorems in the repository, 55 of them in the standard library (`grep -rac '^\s*теорема ' flang --include='*.flang'`). Most postconditions need no theorem: the proof report shows, as a separate number, how many were proved **without a written proof**. diff --git a/docs/site/proofs.ru.md b/docs/site/proofs.ru.md index f57021269..dd9e0e196 100644 --- a/docs/site/proofs.ru.md +++ b/docs/site/proofs.ru.md @@ -64,7 +64,7 @@ руками**, как в Coq или Isabelle. `теорема` пишется по шагам: `дано`, `утверждаем`, `затем … по свойству «…»`, `индукция по …`, `следовательно доказано`. Это читается как Isar в Isabelle, и prover проверяет каждый шаг, -ничего не ища. В дереве языка таких теорем 303, из них 55 в стандартной +ничего не ища. В дереве языка таких теорем 308, из них 55 в стандартной библиотеке (`grep -rac '^\s*теорема ' flang --include='*.flang'`). Большинству постусловий теорема не нужна: отчёт о доказательствах показывает отдельным числом, сколько доказано **без написанного доказательства**. diff --git a/docs/tree-inventory.md b/docs/tree-inventory.md index 679bfae6d..06f54620b 100644 --- a/docs/tree-inventory.md +++ b/docs/tree-inventory.md @@ -77,7 +77,7 @@ $ bootstrap/flang io scripts/guards/tree-inventory.fscript --max-steps 50000000 | язык | файлов | строк | долг файлов | долг строк | |---|---:|---:|---:|---:| | оболочка | 58 | 10 079 | 52 | 5 629 | -| C | 37 | 871 301 | 0 | 0 | +| C | 37 | 871 439 | 0 | 0 | | C++ | 1 | 404 | 0 | 0 | | Python | 5 | 2 906 | 0 | 0 | | HTML | 7 | 1 263 | 0 | 0 | diff --git a/flang/proof/checker/checker.c b/flang/proof/checker/checker.c index c427bae14..c9a78f75f 100644 --- a/flang/proof/checker/checker.c +++ b/flang/proof/checker/checker.c @@ -419,6 +419,11 @@ static char *цель_обещанная(const char *ц) { char *м, *т, *у; return разобрать_существование(ц, &м, &т, &у) ? терм(вставить_вместо(терм(у), м, терм(т))) : (char *)ц; } +static char *со_свидетелем(const char *ц) { + char *м, *т, *у; + if (!разобрать_существование(ц, &м, &т, &у)) return терм(ц); + return терм(вставить_вместо(заменить(заменить(fmt(" %s ", терм(у)), fmt(" %s.", голо(м)), fmt(" %s.", т)), fmt(" «%s».", голо(м)), fmt(" %s.", т)), м, т)); +} /* У утверждения без функции «место» — его заголовок `утверждение «И»` от края, цель — хвост строки `утверждаем`, типы и имена связанных — строки `для всех` @@ -615,9 +620,12 @@ static Сп разметка_теоремы(Сп строки, long начало if (начинается(s, "//") || !*s) continue; if (утв && strspn(сырая, " ") > утв) continue; утв = 0; - вид = начинается(s, "теорема ") || (i == начало && следует) ? "теорема" : вид_строки_теоремы(s); - if (strcmp(вид, "утверждаем") == 0) утв = strspn(сырая, " "); - if (!*вид || (следует && strcmp(вид, "доказано") == 0)) continue; + if (начинается(s, "теорема ") || (i == начало && следует)) вид = "теорема"; + else { + вид = вид_строки_теоремы(s); + if (strcmp(вид, "утверждаем") == 0) утв = strspn(сырая, " "); + if (!*вид || (следует && strcmp(вид, "доказано") == 0)) continue; + } /* К5: `дано <утверждение>` — допущение, а не имя; `дано х: T таких что P` — имя и допущение на одной строке. Допущение запись печатает своей строкой. */ if (strcmp(вид, "дано") == 0 && (!содержит(s, ":") || содержит(s, " таких что "))) { @@ -1862,7 +1870,7 @@ static void сверить_цель(Сверка *s, Сп свои, Сп стр long гв = строка_высказывания(строки, место); /* К3b: утверждение без функции */ char *сырое = гв ? из_высказывания(строки, гв, NULL, NULL) : с_продолжением(строки, номер_после(часть(свои, 1), "строка "), хвост_после(как_читает_язык(место), fmt("обеспечивает «%s» ", имя))); - char *обещано = гв ? терм(цель_обещанная(сырое)) + char *обещано = гв ? со_свидетелем(сырое) : цель_обещанная(сырое); /* К7: у существования — У[м:=Т], как терм */ char *строка_цели = первая_с_началом(свои, "цель "); long где = номер_после(строка_цели, "строка "); @@ -1873,7 +1881,7 @@ static void сверить_цель(Сверка *s, Сп свои, Сп стр сверить_терм_и_номер(s, строка_цели, утверждено, где, имя_т, "цель"); утверждено = с_продолжением(строки, где, утверждено); } - если_не(s, strcmp(обещано, обещано == сырое ? утверждено : терм(утверждено)) == 0, + если_не(s, strcmp(обещано, обещано == сырое ? утверждено : гв ? со_свидетелем(утверждено) : терм(утверждено)) == 0, fmt("теорема «%s» утверждает «%s», а %s обещает «%s» — доказывается не то, что обещано", имя_т, утверждено, гв ? "утверждение" : "постусловие", обещано)); } @@ -3502,13 +3510,109 @@ static void сверить_правило_шага(Сверка *s, const char * } } +typedef struct { Сп строки, имена, атомы; long гв; unsigned long набор; } Посылки; +static Сп связка(const char *t, const char *op) { + Сп ч = разделить_сверху(t, op); int i; + for (i = 0; ч.n > 1 && i < ч.n; i++) if (начинается(обрезать(ч.e[i]), "если ")) return ПУСТО; + return ч; +} +static Сп конъюнкты(const char *сырой) { + char *t = терм(сырой); Сп ч = связка(t, "и притом"), итог = ПУСТО; int i, j; + if (ч.n < 2 || связка(t, "или").n != 1) { добавить(&итог, t); return итог; } + for (i = 0; i < ч.n; i++) { Сп в = конъюнкты(ч.e[i]); for (j = 0; j < в.n; j++) добавить(&итог, в.e[j]); } + return итог; +} +static int признак_ли(Посылки *п, const char *атом) { + int i; long j; + for (i = 0; i < п->имена.n; i++) { + char *т = fmt("объект «%s»", голо(из_высказывания(п->строки, п->гв, п->имена.e[i], NULL))); + for (j = 1; j <= п->строки.n && strcmp(строка_по_номеру(п->строки, j), т) != 0; j++) ; + for (j++; j <= п->строки.n && начинается(часть(п->строки, j), " "); j++) { + char *s = строка_по_номеру(п->строки, j), *поле = голо(часть(разделить(s, ":"), 1)); + if (strcmp(обрезать(хвост_после(s, ":")), "признак") == 0 && + (strcmp(атом, fmt("«%s».«%s»", п->имена.e[i], поле)) == 0 || strcmp(атом, fmt("%s.«%s»", п->имена.e[i], поле)) == 0)) return 1; + } + } + return 0; +} +static int истинно(const char *сырой, Посылки *п) { + char *t = терм(сырой); Сп или = связка(t, "или"), ч = или.n == 1 ? связка(t, "и притом") : или; int i, a, b, c, итог = или.n == 1; + if (strcmp(t, "да") == 0 || strcmp(t, "нет") == 0) return strcmp(t, "да") == 0; + for (i = 0; ч.n > 1 && i < ч.n; i++) { if ((a = истинно(ч.e[i], п)) < 0) return -1; итог = или.n == 1 ? итог && a : итог || a; } + if (ч.n != 1) return ч.n ? итог : -1; + if (начинается(t, "не ")) return (a = истинно(t + strlen("не "), п)) < 0 ? -1 : !a; + if (начинается(t, "если ")) { + Сп то = разделить_сверху(t + strlen("если "), "то"), ин = разделить_сверху(часть(то, 2), "иначе"); + if (то.n != 2 || ин.n != 2 || (a = истинно(то.e[0], п)) < 0 || (b = истинно(ин.e[0], п)) < 0 || (c = истинно(ин.e[1], п)) < 0) return -1; + return a ? b : c; + } + for (i = 0; i < п->атомы.n && strcmp(п->атомы.e[i], t) != 0; i++) ; + if (i == п->атомы.n && (i >= 16 || !признак_ли(п, t))) return -1; + if (i == п->атомы.n) добавить(&п->атомы, t); + return (int)((п->набор >> i) & 1); +} +static long контрпример(Сп K, const char *ф, Посылки *п) { + int i, v; + for (п->набор = 0, п->атомы = ПУСТО, i = 0; i <= K.n; i++) if (истинно(i < K.n ? K.e[i] : ф, п) < 0) return -2; + for (п->набор = 0; п->набор < (1UL << п->атомы.n); п->набор++) { + for (v = 1, i = 0; i < K.n && v; i++) v = истинно(K.e[i], п); + if (v && !истинно(ф, п)) return (long)п->набор; + } + return -1; +} +static int есть_в(Сп K, const char *t) { int i; for (i = 0; i < K.n; i++) if (strcmp(K.e[i], терм(t)) == 0) return 1; return 0; } +static int выводится(Сп K, const char *ф) { + Сп ч = конъюнкты(ф); int i, j, есть; + for (j = 0; j < ч.n; j++) { + for (есть = есть_в(K, ч.e[j]), i = 0; i < K.n && !есть; i++) { + Сп то = разделить_сверху(хвост_после(K.e[i], "если "), "то"), ин = разделить_сверху(часть(то, 2), "иначе"); + есть = начинается(K.e[i], "если ") && то.n == 2 && ин.n == 2 && strcmp(терм(ин.e[1]), "да") == 0 && + strcmp(терм(ин.e[0]), ч.e[j]) == 0 && есть_в(K, то.e[0]); + есть |= strcmp(ч.e[j], "нет") == 0 && начинается(K.e[i], "не ") && есть_в(K, K.e[i] + strlen("не ")); + } + if (!есть) return 0; + } + return 1; +} +static char *формула_шага(Сп строки, const char *ш) { + long где = номер_после(ш, "строка "); char *l = где < 1 ? (char *)"" : без_то(с_продолжением(строки, где, как_читает_язык(строка_по_номеру(строки, где)))); + if (!начинается(l, "затем ") || !содержит(l, " по предположению")) return (char *)""; + return копия(l + strlen("затем "), (size_t)(strstr(l, " по предположению") - l) - strlen("затем ")); +} +static int из_посылок(Сверка *s, Сп свои, Сп строки, long гв, const char *имя_т) { + Посылки п; Сп K = ПУСТО, шаги = все_с_началом(свои, "шаг "), ч; + long i, j, m, до = s->беды.n, гц = номер_после(первая_с_началом(свои, "цель "), "строка "); + char *цель = гц < 1 ? (char *)"" : с_продолжением(строки, гц, хвост_после(как_читает_язык(строка_по_номеру(строки, гц)), "утверждаем ")); + п.строки = строки; п.гв = гв; п.имена = ПУСТО; + из_высказывания(строки, гв, NULL, &п.имена); + if (!гв || гц < 1 || *первая_с_началом(свои, "случай ")) return 0; + for (i = 0; i < шаги.n; i++) if (!начинается(шаг_обоснование(шаги.e[i]), "по предположению")) return 0; + for (i = гв + 1; i <= строки.n; i++) { + char *сырая = часть(строки, i), *l = с_продолжением(строки, i, как_читает_язык(обрезать(без_примечания(сырая)))); + if (*сырая && !начинается(сырая, " ") && !начинается(сырая, "//")) break; + if (начинается(l, "для всех ") && содержит(l, " таких что ")) + for (ч = конъюнкты(хвост_после(l, " таких что ")), j = 0; j < ч.n; j++) добавить(&K, ч.e[j]); + } + for (i = 0; i < шаги.n; i++) { + char *ф = strcmp(шаг_вид(шаги.e[i]), "промежуточный") == 0 ? формула_шага(строки, шаги.e[i]) : со_свидетелем(цель); + if (!*ф || (m = контрпример(K, ф, &п)) == -2) return 0; + if (m >= 0) { Сп при = ПУСТО; + for (j = 0; j < п.атомы.n; j++) добавить(&при, fmt("%s %s", п.атомы.e[j], (m >> j) & 1 ? "да" : "нет")); + добавить(&s->беды, fmt("теорема «%s»: шаг %s ⟨%s⟩ из посылок утверждения не следует — при %s посылки верны, а он ложен", имя_т, слово(шаги.e[i], 2), терм(ф), соединить(при, ", "))); + return 0; } + if (!выводится(K, ф)) return 0; + добавить(&K, терм(ф)); + } + return s->беды.n == до; +} + static void сверить_шаги(Сверка *s, Сп свои, Сп строки, const char *имя_т, - const char *чья, const char *цель) { + const char *чья, const char *цель, const char *место) { char *по = в_ёлочках(первая_с_началом(свои, "индукция по "), 1); /* Свободное имя в цели: `дано «х»` или индукция. Тогда `результат` не одно значение, и подстановка тела (дорога Ч76) не годится — «не берусь». */ int свободные = (*первая_с_началом(свои, "дано «") != 0) || (*по != 0); - long случай_где = 0; int i; + long случай_где = 0, гв = строка_высказывания(строки, место); int i, посылками = !*по && из_посылок(s, свои, строки, гв, имя_т); for (i = 0; i < свои.n; i++) { char *ш = обрезать(свои.e[i]); long где; char *вид, *обоснование, *в_исх; @@ -3519,7 +3623,7 @@ static void сверить_шаги(Сверка *s, Сп свои, Сп стр /* «по предположению допущение J»: J обязано быть среди допущений записи, сам вывод — на слове ядра. В исходнике шаг написан без номера, потому обоснование и урезается. */ if (начинается(обоснование, "по предположению допущение ")) { - long J = номер_после(обоснование, "допущение "), всего = все_с_началом(свои, "допущение ").n; + long J = номер_после(обоснование, "допущение "), всего = все_с_началом(свои, "допущение ").n + (гв ? ограничения_высказывания(строки, место).n : 0); если_не(s, J >= 1 && J <= всего, fmt("теорема «%s»: шаг %s закрыт допущением %ld, а допущений в записи %ld", имя_т, слово(ш, 2), J, всего)); @@ -3550,6 +3654,8 @@ static void сверить_шаги(Сверка *s, Сп свои, Сп стр предположению»: допущение у неё одно — предусловие функции, и шаг верен ровно тогда, когда тело неотрицательно по построению при этом допущении. */ s->сведений++; s->шагов_по_телу++; + } else if (посылками && strcmp(обоснование, "по предположению") == 0) { + s->сведений++; } else { /* Ветвь ловит ЛЮБОЕ обоснование, а не список имён: имя, не попавшее ни в одну ветвь, не было бы ни проверено, ни положено в долг — и пять дописанных строк @@ -8813,6 +8919,37 @@ static void сверить_разметку_теоремы(Сверка *s, Сп имя_т, j + 1, в_уголках(доп.e[j], 1), где_д, P)); } } } +static int среди_конъюнктов(const char *гипотеза, const char *ограничение) { + Сп части = разделить_сверху(терм(ограничение), "и притом"); int j; + if (части.n < 2) return совпали_цели(гипотеза, терм(ограничение)); + for (j = 0; j < части.n; j++) if (среди_конъюнктов(гипотеза, части.e[j])) return 1; + return 0; +} +static char *тип_переменной(Сп строки, const char *место, const char *чья, const char *имя) { + Доводы д; int k; + if (строка_высказывания(строки, место)) return из_высказывания(строки, строка_высказывания(строки, место), имя, NULL); + д = доводы_функции(строки, чья); + for (k = 0; k < д.имена.n; k++) if (strcmp(голо(д.имена.e[k]), имя) == 0) return д.типы.e[k]; + return (char *)""; +} +static int факт_типа(const char *гипотеза, Сп строки, const char *место, const char *чья) { + Разрез r = разрез_по(гипотеза, "не меньше"); + if (!r.есть || strcmp(ужать(r.право), "0") != 0) return 0; + return натуральное_имя(имя_типа(тип_переменной(строки, место, чья, голо(ужать(r.лево))))); +} +static void сверить_снятие_гипотез(Сверка *s, Сп свои, Сп строки, const char *имя_т, const char *место, const char *чья) { + Сп доп = все_с_началом(свои, "допущение "), тч = все_с_началом(свои, "таких что "), огр = ПУСТО; + Сп треб = строка_высказывания(строки, место) ? ПУСТО : все_требования_функции(строки, чья); int i, j; + for (j = 0; j < тч.n; j++) добавить(&огр, в_уголках(тч.e[j], 1)); + for (j = 0; j < треб.n; j++) добавить(&огр, формула_требования(треб.e[j])); + for (i = 0; i < доп.n; i++) { + char *г = терм(в_уголках(доп.e[i], 1)); int снята = факт_типа(г, строки, место, чья); + for (j = 0; j < огр.n && !снята; j++) снята = среди_конъюнктов(г, огр.e[j]); + если_не(s, снята, + fmt("теорема «%s»: гипотеза ⟨%s⟩ строки %ld не является допущением утверждения — её нет ни в «таких что», ни в «требует», ни в объявленном типе", + имя_т, в_уголках(доп.e[i], 1), номер_после(доп.e[i], "строка "))); + } +} static void сверить_теорему(Сверка *s, Сп свои, Сп строки, const char *вердикт, const char *место, const char *имя, const char *чья) { char *строка_т = первая_с_началом(свои, "теорема «"); @@ -8822,6 +8959,7 @@ static void сверить_теорему(Сверка *s, Сп свои, Сп long не_проигрываемых_до = 0, моих_не_проигрываемых; long законом_до = 0; сверить_разметку_теоремы(s, свои, строки, имя_т, начало); + сверить_снятие_гипотез(s, свои, строки, имя_т, место, чья); сверить_цель(s, свои, строки, место, имя, имя_т); сверить_имена(s, свои, строки, имя_т); сверить_число_шагов(s, свои, имя_т); @@ -8832,7 +8970,7 @@ static void сверить_теорему(Сверка *s, Сп свои, Сп не_проигрываемых_до = s->шагов_не_проигрываемых; законом_до = s->шагов_законом; сверить_шаги(s, свои, строки, имя_т, чья, - гц < 1 ? в_уголках(ск, 1) : хвост_после(как_читает_язык(строка_по_номеру(строки, гц)), "утверждаем ")); } + гц < 1 ? в_уголках(ск, 1) : хвост_после(как_читает_язык(строка_по_номеру(строки, гц)), "утверждаем "), место); } сверить_закрытие(s, свои, имя_т, вердикт); сверить_правила(s, свои, fmt("теорема «%s»", имя_т)); /* Места снимаются РОВНО те, что начислила ветвь «по закону» (разница diff --git a/flang/proof/checker/tests/families/assumption-replay/affirming-the-consequent.record b/flang/proof/checker/tests/families/assumption-replay/affirming-the-consequent.record new file mode 100644 index 000000000..62375ead2 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/affirming-the-consequent.record @@ -0,0 +1,24 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/affirming-the-consequent.flang +строк 17 +знаков 465 +отпечаток 745919929 6196609 +ядро 2 +утверждений 1 +отпечаток256 d569dcd7796b6b754268e1f9b5abf69ee639e7a0f1437731ce70dab8e89361cb + +утверждение «Сократ — человек» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «Сократ».«человек» то «Сократ».«смертен» иначе да ) и притом «Сократ».«смертен»⟩ строка 8 + вердикт доказано + теорема «Сократ — человек» строка 11 + дано «Сократ» строка 12 + допущение ⟨если «Сократ».«человек» то «Сократ».«смертен» иначе да⟩ строка 13 + допущение ⟨«Сократ».«смертен»⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/barbara-without-the-middle-step.record b/flang/proof/checker/tests/families/assumption-replay/barbara-without-the-middle-step.record new file mode 100644 index 000000000..02d587e75 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/barbara-without-the-middle-step.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/barbara-without-the-middle-step.flang +строк 19 +знаков 603 +отпечаток 411755632 493253088 +ядро 2 +утверждений 1 +отпечаток256 413625bde79b57aa18eccf452707829bd5281fee1a836703dcccdc027cb5f3fa + +утверждение «все греки смертны» строка 8 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «всякий».«человек» то «всякий».«смертен» иначе да ) и притом ( если «всякий».«грек» то «всякий».«человек» иначе да ) и притом «всякий».«грек»⟩ строка 9 + вердикт доказано + теорема «все греки смертны» строка 12 + дано «всякий» строка 13 + допущение ⟨если «всякий».«человек» то «всякий».«смертен» иначе да⟩ строка 14 + допущение ⟨если «всякий».«грек» то «всякий».«человек» иначе да⟩ строка 15 + допущение ⟨«всякий».«грек»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/barbara.record b/flang/proof/checker/tests/families/assumption-replay/barbara.record new file mode 100644 index 000000000..442013760 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/barbara.record @@ -0,0 +1,26 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/barbara.flang +строк 20 +знаков 647 +отпечаток 786208141 188328047 +ядро 2 +утверждений 1 +отпечаток256 b27f9b40eb88525d04697198d80ad4f0003d0f62807c4292d2b3e3deae3ec978 + +утверждение «все греки смертны» строка 8 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «всякий».«человек» то «всякий».«смертен» иначе да ) и притом ( если «всякий».«грек» то «всякий».«человек» иначе да ) и притом «всякий».«грек»⟩ строка 9 + вердикт доказано + теорема «все греки смертны» строка 12 + дано «всякий» строка 13 + допущение ⟨если «всякий».«человек» то «всякий».«смертен» иначе да⟩ строка 14 + допущение ⟨если «всякий».«грек» то «всякий».«человек» иначе да⟩ строка 15 + допущение ⟨«всякий».«грек»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 промежуточный по предположению правило «цель есть допущение» + шаг 2 строка 19 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/camestres-by-refutation.record b/flang/proof/checker/tests/families/assumption-replay/camestres-by-refutation.record new file mode 100644 index 000000000..8aec8c596 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/camestres-by-refutation.record @@ -0,0 +1,28 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/camestres-by-refutation.flang +строк 22 +знаков 756 +отпечаток 579803564 147320406 +ядро 2 +утверждений 1 +отпечаток256 f6f0058f1452bbf0d6e5710eb3e5b1f1ac7f28324ac6ce2e7153499bf8a06be0 + +утверждение «ни один кит не рыба» строка 8 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «всякий».«рыба» то «всякий».«дышит жабрами» иначе да ) и притом ( если «всякий».«кит» то ( не «всякий».«дышит жабрами» ) иначе да ) и притом «всякий».«кит» и притом «всякий».«рыба»⟩ строка 9 + вердикт доказано + теорема «ни один кит не рыба» строка 12 + дано «всякий» строка 13 + допущение ⟨если «всякий».«рыба» то «всякий».«дышит жабрами» иначе да⟩ строка 14 + допущение ⟨если «всякий».«кит» то ( не «всякий».«дышит жабрами» ) иначе да⟩ строка 15 + допущение ⟨«всякий».«кит»⟩ строка 16 + допущение ⟨«всякий».«рыба»⟩ строка 17 + цель строка 18 + шаг 1 строка 19 промежуточный по предположению правило «цель есть допущение» + шаг 2 строка 20 промежуточный по предположению правило «цель есть допущение» + шаг 3 строка 21 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/celarent.record b/flang/proof/checker/tests/families/assumption-replay/celarent.record new file mode 100644 index 000000000..c6d82da39 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/celarent.record @@ -0,0 +1,26 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/celarent.flang +строк 20 +знаков 655 +отпечаток 637001399 380025156 +ядро 2 +утверждений 1 +отпечаток256 7e344796c7cce2a3e398d676e8b7fe448b3274d8e46f57d73ce98dc4565e73d1 + +утверждение «ни один кашалот не рыба» строка 8 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «всякий».«кит» то ( не «всякий».«рыба» ) иначе да ) и притом ( если «всякий».«кашалот» то «всякий».«кит» иначе да ) и притом «всякий».«кашалот»⟩ строка 9 + вердикт доказано + теорема «ни один кашалот не рыба» строка 12 + дано «всякий» строка 13 + допущение ⟨если «всякий».«кит» то ( не «всякий».«рыба» ) иначе да⟩ строка 14 + допущение ⟨если «всякий».«кашалот» то «всякий».«кит» иначе да⟩ строка 15 + допущение ⟨«всякий».«кашалот»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 промежуточный по предположению правило «цель есть допущение» + шаг 2 строка 19 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/darii-with-the-existence-word.record b/flang/proof/checker/tests/families/assumption-replay/darii-with-the-existence-word.record new file mode 100644 index 000000000..f77153a49 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/darii-with-the-existence-word.record @@ -0,0 +1,27 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/darii-with-the-existence-word.flang +строк 19 +знаков 810 +отпечаток 998230778 390332762 +ядро 2 +утверждений 1 +отпечаток256 f1a2e9e09d35fc4c5a44e7a701d8943eb69c8e93c70927d9f639849447f195c1 + +утверждение «некоторые питомцы мохнаты» строка 8 + вид statement + для всех «предмет посылки 2» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да ) и притом «предмет посылки 2».«питомец» и притом «предмет посылки 2».«кролик»⟩ строка 9 + свидетель «некий» ⟨«предмет посылки 2»⟩ строка 10 + после подстановки ⟨некий.«питомец» и притом некий.«мохнат»⟩ + вердикт доказано + теорема «некоторые питомцы мохнаты» строка 12 + дано «предмет посылки 2» строка 13 + допущение ⟨если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да⟩ строка 14 + допущение ⟨«предмет посылки 2».«питомец»⟩ строка 15 + допущение ⟨«предмет посылки 2».«кролик»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 закрывающий по предположению допущение 1 правило «разбор цели по условию» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/darii.record b/flang/proof/checker/tests/families/assumption-replay/darii.record new file mode 100644 index 000000000..ce4507e77 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/darii.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/darii.flang +строк 19 +знаков 762 +отпечаток 362413914 663275733 +ядро 2 +утверждений 1 +отпечаток256 8543cadffbb3d78793b799b7ae2bc1aed77d6e198b8dd84179c5d85caee15940 + +утверждение «некоторые питомцы мохнаты» строка 8 + вид statement + для всех «предмет посылки 2» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да ) и притом «предмет посылки 2».«питомец» и притом «предмет посылки 2».«кролик»⟩ строка 9 + вердикт доказано + теорема «некоторые питомцы мохнаты» строка 12 + дано «предмет посылки 2» строка 13 + допущение ⟨если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да⟩ строка 14 + допущение ⟨«предмет посылки 2».«питомец»⟩ строка 15 + допущение ⟨«предмет посылки 2».«кролик»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 закрывающий по предположению допущение 1 правило «разбор цели по условию» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/denying-the-antecedent.record b/flang/proof/checker/tests/families/assumption-replay/denying-the-antecedent.record new file mode 100644 index 000000000..748db2aca --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/denying-the-antecedent.record @@ -0,0 +1,24 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/denying-the-antecedent.flang +строк 17 +знаков 487 +отпечаток 640233816 30024500 +ядро 2 +утверждений 1 +отпечаток256 606f0c3f7865157bc049e3388d466887c71e4a95577a5567da1f11ba455fa283 + +утверждение «Сократ не смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «Сократ».«человек» то «Сократ».«смертен» иначе да ) и притом ( не «Сократ».«человек» )⟩ строка 8 + вердикт доказано + теорема «Сократ не смертен» строка 11 + дано «Сократ» строка 12 + допущение ⟨если «Сократ».«человек» то «Сократ».«смертен» иначе да⟩ строка 13 + допущение ⟨не «Сократ».«человек»⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/existential-import.record b/flang/proof/checker/tests/families/assumption-replay/existential-import.record new file mode 100644 index 000000000..1d4621185 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/existential-import.record @@ -0,0 +1,24 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/existential-import.flang +строк 18 +знаков 607 +отпечаток 767872960 659549136 +ядро 2 +утверждений 1 +отпечаток256 8a6c09850cd91cfdc57783461d805d868dcd5e67cd65c6692d0482560ea42522 + +утверждение «некоторые греки смертны» строка 8 + вид statement + для всех «некий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «некий».«человек» то «некий».«смертен» иначе да ) и притом ( если «некий».«грек» то «некий».«человек» иначе да )⟩ строка 9 + вердикт доказано + теорема «некоторые греки смертны» строка 12 + дано «некий» строка 13 + допущение ⟨если «некий».«человек» то «некий».«смертен» иначе да⟩ строка 14 + допущение ⟨если «некий».«грек» то «некий».«человек» иначе да⟩ строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по предположению допущение 1 правило «разбор цели по условию» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/ferio.record b/flang/proof/checker/tests/families/assumption-replay/ferio.record new file mode 100644 index 000000000..afefdf358 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/ferio.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/ferio.flang +строк 19 +знаков 824 +отпечаток 256091376 224009567 +ядро 2 +утверждений 1 +отпечаток256 5557d980818a55d74a5ea4be4fec92c7f23968fe8b1466a03e4d867f8dcba5d3 + +утверждение «некоторые морские животные — не рыбы» строка 8 + вид statement + для всех «предмет посылки 2» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «предмет посылки 2».«кит» то ( не «предмет посылки 2».«рыба» ) иначе да ) и притом «предмет посылки 2».«морское животное» и притом «предмет посылки 2».«кит»⟩ строка 9 + вердикт доказано + теорема «некоторые морские животные — не рыбы» строка 12 + дано «предмет посылки 2» строка 13 + допущение ⟨если «предмет посылки 2».«кит» то ( не «предмет посылки 2».«рыба» ) иначе да⟩ строка 14 + допущение ⟨«предмет посылки 2».«морское животное»⟩ строка 15 + допущение ⟨«предмет посылки 2».«кит»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 закрывающий по предположению допущение 1 правило «разбор цели по условию» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/illicit-conversion.record b/flang/proof/checker/tests/families/assumption-replay/illicit-conversion.record new file mode 100644 index 000000000..c7255e622 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/illicit-conversion.record @@ -0,0 +1,24 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/illicit-conversion.flang +строк 17 +знаков 476 +отпечаток 820816676 230149327 +ядро 2 +утверждений 1 +отпечаток256 e5523a4e2fe55d68ffb208d6c17928254590c808426e0eb3644ce039e72b9251 + +утверждение «все смертные — люди» строка 7 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «всякий».«человек» то «всякий».«смертный» иначе да ) и притом «всякий».«смертный»⟩ строка 8 + вердикт доказано + теорема «все смертные — люди» строка 11 + дано «всякий» строка 12 + допущение ⟨если «всякий».«человек» то «всякий».«смертный» иначе да⟩ строка 13 + допущение ⟨«всякий».«смертный»⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang b/flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang new file mode 100644 index 000000000..71cbc848f --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang @@ -0,0 +1,17 @@ +модуль «Reasoning» + +объект «Предмет» + «человек»: признак + «смертен»: признак + +утверждение «Платон смертен» + для всех «Сократ»: «Предмет» и «Платон»: «Предмет» таких что (если «Сократ».«человек» то «Сократ».«смертен» иначе да) и притом «Платон».«человек» + утверждаем «Платон».«смертен» + +следует «Платон смертен» + дано «Сократ»: «Предмет» + дано «Платон»: «Предмет» + дано (если «Сократ».«человек» то «Сократ».«смертен» иначе да) + дано «Платон».«человек» + утверждаем «Платон».«смертен» + по предположению diff --git a/flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.record b/flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.record new file mode 100644 index 000000000..6b6d50d7d --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.record @@ -0,0 +1,26 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang +строк 18 +знаков 510 +отпечаток 544359786 38607868 +ядро 2 +утверждений 1 +отпечаток256 718bac3e5da72d464ae901264d3b23e7a17c487f5c0d9a400f8589f6a914a67d + +утверждение «Платон смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + для всех «Платон» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «Сократ».«человек» то «Сократ».«смертен» иначе да ) и притом «Платон».«человек»⟩ строка 8 + вердикт доказано + теорема «Платон смертен» строка 11 + дано «Сократ» строка 12 + дано «Платон» строка 13 + допущение ⟨если «Сократ».«человек» то «Сократ».«смертен» иначе да⟩ строка 14 + допущение ⟨«Платон».«человек»⟩ строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang b/flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang new file mode 100644 index 000000000..f7ca16c2c --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang @@ -0,0 +1,17 @@ +модуль «Reasoning» + +объект «Предмет» + «человек»: признак + «смертен»: признак + +утверждение «Платон смертен» + для всех «Сократ»: «Предмет» и «Платон»: «Предмет» таких что (если «Платон».«человек» то «Платон».«смертен» иначе да) и притом «Платон».«человек» + утверждаем «Платон».«смертен» + +следует «Платон смертен» + дано «Сократ»: «Предмет» + дано «Платон»: «Предмет» + дано (если «Платон».«человек» то «Платон».«смертен» иначе да) + дано «Платон».«человек» + утверждаем «Платон».«смертен» + по предположению diff --git a/flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.record b/flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.record new file mode 100644 index 000000000..7448a84dd --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.record @@ -0,0 +1,26 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang +строк 18 +знаков 510 +отпечаток 437455559 709052247 +ядро 2 +утверждений 1 +отпечаток256 ec47c9c2170cb1d646ce2bdd892946d1e2de5d481eeae5a354779a4378a900aa + +утверждение «Платон смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + для всех «Платон» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «Платон».«человек» то «Платон».«смертен» иначе да ) и притом «Платон».«человек»⟩ строка 8 + вердикт доказано + теорема «Платон смертен» строка 11 + дано «Сократ» строка 12 + дано «Платон» строка 13 + допущение ⟨если «Платон».«человек» то «Платон».«смертен» иначе да⟩ строка 14 + допущение ⟨«Платон».«человек»⟩ строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/premises-only-in-the-statement.record b/flang/proof/checker/tests/families/assumption-replay/premises-only-in-the-statement.record new file mode 100644 index 000000000..a1571512d --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/premises-only-in-the-statement.record @@ -0,0 +1,22 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-statement.flang +строк 15 +знаков 371 +отпечаток 110395995 20177584 +ядро 2 +утверждений 1 +отпечаток256 3168b04a79c3b6c6d3f4606be3ca8a90411bc054d938e89da97d9ded4cc5909b + +утверждение «Сократ смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «Сократ».«человек» то «Сократ».«смертен» иначе да ) и притом «Сократ».«человек»⟩ строка 8 + вердикт доказано + теорема «Сократ смертен» строка 11 + дано «Сократ» строка 12 + цель строка 13 + шаг 1 строка 14 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.flang b/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.flang new file mode 100644 index 000000000..0977d34fc --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.flang @@ -0,0 +1,20 @@ +модуль «Reasoning» + +объект «Предмет» + «рыба»: признак + «кит»: признак + «дышит жабрами»: признак + +утверждение «ни один кит не рыба» + для всех «всякий»: «Предмет» таких что (если «всякий».«рыба» то «всякий».«дышит жабрами» иначе да) и притом (если «всякий».«кит» то (не «всякий».«дышит жабрами») иначе да) и притом «всякий».«кит» + утверждаем нет + +следует «ни один кит не рыба» + дано «всякий»: «Предмет» + дано (если «всякий».«рыба» то «всякий».«дышит жабрами» иначе да) + дано (если «всякий».«кит» то (не «всякий».«дышит жабрами») иначе да) + дано «всякий».«кит» + утверждаем нет + затем «всякий».«дышит жабрами» по предположению + затем (не «всякий».«дышит жабрами») по предположению + по предположению diff --git a/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.record b/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.record new file mode 100644 index 000000000..9e5774453 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.record @@ -0,0 +1,27 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.flang +строк 21 +знаков 708 +отпечаток 861696332 871310597 +ядро 2 +утверждений 1 +отпечаток256 0a466dbdd5ce96a786c5b2609fada98d827810335cba8687ed81ae077194a96c + +утверждение «ни один кит не рыба» строка 8 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «всякий».«рыба» то «всякий».«дышит жабрами» иначе да ) и притом ( если «всякий».«кит» то ( не «всякий».«дышит жабрами» ) иначе да ) и притом «всякий».«кит»⟩ строка 9 + вердикт доказано + теорема «ни один кит не рыба» строка 12 + дано «всякий» строка 13 + допущение ⟨если «всякий».«рыба» то «всякий».«дышит жабрами» иначе да⟩ строка 14 + допущение ⟨если «всякий».«кит» то ( не «всякий».«дышит жабрами» ) иначе да⟩ строка 15 + допущение ⟨«всякий».«кит»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 промежуточный по предположению правило «цель есть допущение» + шаг 2 строка 19 промежуточный по предположению правило «цель есть допущение» + шаг 3 строка 20 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/undistributed-middle.record b/flang/proof/checker/tests/families/assumption-replay/undistributed-middle.record new file mode 100644 index 000000000..1cd462a32 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/undistributed-middle.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/undistributed-middle.flang +строк 19 +знаков 606 +отпечаток 830748764 757639856 +ядро 2 +утверждений 1 +отпечаток256 6d705a4cf463d5a16fda5e7956e82a0f006d428aae393f6828118b34ec2ac21f + +утверждение «все кошки — люди» строка 8 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «всякий».«человек» то «всякий».«смертен» иначе да ) и притом ( если «всякий».«кошка» то «всякий».«смертен» иначе да ) и притом «всякий».«кошка»⟩ строка 9 + вердикт доказано + теорема «все кошки — люди» строка 12 + дано «всякий» строка 13 + допущение ⟨если «всякий».«человек» то «всякий».«смертен» иначе да⟩ строка 14 + допущение ⟨если «всякий».«кошка» то «всякий».«смертен» иначе да⟩ строка 15 + допущение ⟨«всякий».«кошка»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.flang b/flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.flang new file mode 100644 index 000000000..21ac9737b --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.flang @@ -0,0 +1,19 @@ +модуль «Reasoning» + +объект «Предмет» + «кролик»: признак + «питомец»: признак + «мохнат»: признак + +утверждение «некоторые питомцы мохнаты» + для всех «предмет посылки 2»: «Предмет» и «другой»: «Предмет» таких что (если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да) и притом «предмет посылки 2».«питомец» и притом «предмет посылки 2».«кролик» + утверждаем есть такой некий, а именно «предмет посылки 2», что (некий.«питомец» и притом некий.«мохнат») + +следует «некоторые питомцы мохнаты» + дано «предмет посылки 2»: «Предмет» + дано «другой»: «Предмет» + дано (если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да) + дано «предмет посылки 2».«питомец» + дано «предмет посылки 2».«кролик» + утверждаем есть такой некий, а именно «другой», что (некий.«питомец» и притом некий.«мохнат») + по предположению diff --git a/flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.record b/flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.record new file mode 100644 index 000000000..01c232b30 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.record @@ -0,0 +1,29 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.flang +строк 20 +знаков 848 +отпечаток 541359540 226813889 +ядро 2 +утверждений 1 +отпечаток256 edd60e73406f107b8e73c1c349b55882028b3ca5099e170a8abc837ade33d405 + +утверждение «некоторые питомцы мохнаты» строка 8 + вид statement + для всех «предмет посылки 2» ⟨«Предмет»⟩ строка 9 + для всех «другой» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да ) и притом «предмет посылки 2».«питомец» и притом «предмет посылки 2».«кролик»⟩ строка 9 + свидетель «некий» ⟨«предмет посылки 2»⟩ строка 10 + после подстановки ⟨некий.«питомец» и притом некий.«мохнат»⟩ + вердикт доказано + теорема «некоторые питомцы мохнаты» строка 12 + дано «предмет посылки 2» строка 13 + дано «другой» строка 14 + допущение ⟨если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да⟩ строка 15 + допущение ⟨«предмет посылки 2».«питомец»⟩ строка 16 + допущение ⟨«предмет посылки 2».«кролик»⟩ строка 17 + цель строка 18 + шаг 1 строка 19 закрывающий по предположению допущение 1 правило «разбор цели по условию» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang b/flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang new file mode 100644 index 000000000..75ef54b8e --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang @@ -0,0 +1,19 @@ +модуль «Reasoning» + +объект «Предмет» + «кролик»: признак + «питомец»: признак + «мохнат»: признак + +утверждение «некоторые питомцы мохнаты» + для всех «предмет посылки 2»: «Предмет» и «другой»: «Предмет» таких что (если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да) и притом «предмет посылки 2».«питомец» и притом «предмет посылки 2».«кролик» + утверждаем есть такой некий, а именно «другой», что (некий.«питомец» и притом некий.«мохнат») + +следует «некоторые питомцы мохнаты» + дано «предмет посылки 2»: «Предмет» + дано «другой»: «Предмет» + дано (если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да) + дано «предмет посылки 2».«питомец» + дано «предмет посылки 2».«кролик» + утверждаем есть такой некий, а именно «другой», что (некий.«питомец» и притом некий.«мохнат») + по предположению diff --git a/flang/proof/checker/tests/families/assumption-replay/witness-without-premises.record b/flang/proof/checker/tests/families/assumption-replay/witness-without-premises.record new file mode 100644 index 000000000..d0599944e --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/witness-without-premises.record @@ -0,0 +1,29 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang +строк 20 +знаков 837 +отпечаток 823082656 240630876 +ядро 2 +утверждений 1 +отпечаток256 7d08c713aa53050e9bc4bd7ee467aef3d74b2679ccc42fff18b4e51839986566 + +утверждение «некоторые питомцы мохнаты» строка 8 + вид statement + для всех «предмет посылки 2» ⟨«Предмет»⟩ строка 9 + для всех «другой» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да ) и притом «предмет посылки 2».«питомец» и притом «предмет посылки 2».«кролик»⟩ строка 9 + свидетель «некий» ⟨«другой»⟩ строка 10 + после подстановки ⟨некий.«питомец» и притом некий.«мохнат»⟩ + вердикт доказано + теорема «некоторые питомцы мохнаты» строка 12 + дано «предмет посылки 2» строка 13 + дано «другой» строка 14 + допущение ⟨если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да⟩ строка 15 + допущение ⟨«предмет посылки 2».«питомец»⟩ строка 16 + допущение ⟨«предмет посылки 2».«кролик»⟩ строка 17 + цель строка 18 + шаг 1 строка 19 закрывающий по предположению допущение 1 правило «разбор цели по условию» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang b/flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang new file mode 100644 index 000000000..3301ed481 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang @@ -0,0 +1,18 @@ +модуль «Гипотеза из предусловия» + +тотальная функция «Тождество» + принимает н: число + возвращает число + требует «положительно» н больше 0 + обеспечивает «результат положителен» результат больше 0 + пример «Единица остаётся единицей» + дано н равно 1 + ожидается 1 + н + +теорема «результат положителен» + дано н: число + дано н больше 0 + утверждаем результат больше 0 + по предположению + следовательно доказано diff --git a/flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.record b/flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.record new file mode 100644 index 000000000..b42b946d1 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang +строк 19 +знаков 417 +отпечаток 696440175 224234539 +ядро 2 +утверждений 1 +отпечаток256 1279e243d184054e95dc9a025d414538529010952c6bd30f148e08ee3829a412 +тотальностей 1 +утверждение «результат положителен» функции «Тождество» строка 7 + вид postcondition + вердикт доказано + теорема «результат положителен» строка 13 + дано «н» строка 14 + допущение ⟨н больше 0⟩ строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Тождество» строка 3 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang b/flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang new file mode 100644 index 000000000..8742275bd --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang @@ -0,0 +1,18 @@ +модуль «Гипотеза мимо предусловия» + +тотальная функция «Тождество» + принимает н: число + возвращает число + требует «не больше десяти» н не больше 10 + обеспечивает «результат положителен» результат больше 0 + пример «Единица остаётся единицей» + дано н равно 1 + ожидается 1 + н + +теорема «результат положителен» + дано н: число + дано н больше 0 + утверждаем результат больше 0 + по предположению + следовательно доказано diff --git a/flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.record b/flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.record new file mode 100644 index 000000000..e54c8bc78 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang +строк 19 +знаков 427 +отпечаток 245808399 123859526 +ядро 2 +утверждений 1 +отпечаток256 dcc574881f36a2482bcb690dcb018a33be15a742a253e36c174aa886cc41e07b +тотальностей 1 +утверждение «результат положителен» функции «Тождество» строка 7 + вид postcondition + вердикт доказано + теорема «результат положителен» строка 13 + дано «н» строка 14 + допущение ⟨н больше 0⟩ строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Тождество» строка 3 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/hypothesis/statement-carries-the-hypothesis.record b/flang/proof/checker/tests/families/hypothesis/statement-carries-the-hypothesis.record new file mode 100644 index 000000000..5c4731ad9 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/statement-carries-the-hypothesis.record @@ -0,0 +1,24 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/socrates.flang +строк 17 +знаков 461 +отпечаток 696832843 458177874 +ядро 2 +утверждений 1 +отпечаток256 30c4cfb03e306871c94db8e1879248dc19bc8a776cd9491225cc8f9ade6c57e7 + +утверждение «Сократ смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «Сократ».«человек» то «Сократ».«смертен» иначе да ) и притом «Сократ».«человек»⟩ строка 8 + вердикт доказано + теорема «Сократ смертен» строка 11 + дано «Сократ» строка 12 + допущение ⟨если «Сократ».«человек» то «Сократ».«смертен» иначе да⟩ строка 13 + допущение ⟨«Сократ».«человек»⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/hypothesis/statement-does-not-carry-the-hypothesis.record b/flang/proof/checker/tests/families/hypothesis/statement-does-not-carry-the-hypothesis.record new file mode 100644 index 000000000..b78dfdc35 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/statement-does-not-carry-the-hypothesis.record @@ -0,0 +1,23 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-theorem.flang +строк 17 +знаков 366 +отпечаток 53964851 273723984 +ядро 2 +утверждений 1 +отпечаток256 861637269d91bffa21c869b2793bf0a4c52406d3f2bab7804e55e85f1708e310 + +утверждение «Сократ смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + вердикт доказано + теорема «Сократ смертен» строка 11 + дано «Сократ» строка 12 + допущение ⟨если «Сократ».«человек» то «Сократ».«смертен» иначе да⟩ строка 13 + допущение ⟨«Сократ».«человек»⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 2 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang b/flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang new file mode 100644 index 000000000..109b6d776 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang @@ -0,0 +1,17 @@ +модуль «Гипотеза из объявленного типа» + +тотальная функция «Тождество» + принимает н: неотрицательное + возвращает неотрицательное + обеспечивает «результат не меньше нуля» результат не меньше 0 + пример «Единица остаётся единицей» + дано н равно 1 + ожидается 1 + н + +теорема «результат не меньше нуля» + дано н: неотрицательное + дано н не меньше 0 + утверждаем результат не меньше 0 + по предположению + следовательно доказано diff --git a/flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.record b/flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.record new file mode 100644 index 000000000..0bc911fdd --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang +строк 18 +знаков 432 +отпечаток 674178374 56366058 +ядро 2 +утверждений 1 +отпечаток256 27af15a89c5716f575d535a2b49c0fab83f206fbe20cc513a847b284f89775be +тотальностей 1 +утверждение «результат не меньше нуля» функции «Тождество» строка 6 + вид postcondition + вердикт доказано + теорема «результат не меньше нуля» строка 12 + дано «н» строка 13 + допущение ⟨н не меньше 0⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Тождество» строка 3 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang b/flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang new file mode 100644 index 000000000..07d7e1842 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang @@ -0,0 +1,17 @@ +модуль «Гипотеза мимо объявленного типа» + +тотальная функция «Тождество» + принимает н: целое + возвращает целое + обеспечивает «результат не меньше нуля» результат не меньше 0 + пример «Единица остаётся единицей» + дано н равно 1 + ожидается 1 + н + +теорема «результат не меньше нуля» + дано н: целое + дано н не меньше 0 + утверждаем результат не меньше 0 + по предположению + следовательно доказано diff --git a/flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.record b/flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.record new file mode 100644 index 000000000..537937eed --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang +строк 18 +знаков 404 +отпечаток 87906575 656688072 +ядро 2 +утверждений 1 +отпечаток256 5f7411a5e4db417cffb087a8d728a0870521e331bceff832ba47dc666c8791ae +тотальностей 1 +утверждение «результат не меньше нуля» функции «Тождество» строка 6 + вид postcondition + вердикт доказано + теорема «результат не меньше нуля» строка 12 + дано «н» строка 13 + допущение ⟨н не меньше 0⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Тождество» строка 3 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/probes.tsv b/flang/proof/checker/tests/probes.tsv index 308170266..8bd0fc4f4 100644 --- a/flang/proof/checker/tests/probes.tsv +++ b/flang/proof/checker/tests/probes.tsv @@ -499,7 +499,7 @@ say - - - - - - - - - - say ── семья «ограничение» (ADR-0026 К5): «таких что» и допущения теоремы ── - - - - - - - - - - C ограничение: постусловие «таких что», строки есть (честная) flang/proof/checker/tests/families/restriction/f09-restricted.flang flang/proof/checker/tests/families/restriction/f09-restricted.record - - - - 3 - - - C ограничение: теорема «дано н: … таких что …», шаг по допущению 1 (честная) flang/proof/checker/tests/families/restriction/k2bk-theorem-such-that.flang flang/proof/checker/tests/families/restriction/k2bk-theorem-such-that.record - - - - 3 - - - -C ограничение: теорема с гипотезой «дано н больше 0» (честная) flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.flang flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.record - - - - 3 - - - +P ограничение: гипотеза «дано н больше 0», которой у постусловия нет flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.flang flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.record - - - - 1 не является допущением утверждения - - P ограничение: потеряно — запись З10 матрицы (прежде код 3) flang/proof/checker/tests/families/restriction/f09-restricted.flang flang/proof/checker/tests/families/restriction/corrupt/z10-restriction-lost.record - - - - 1 ограничение потеряно - - P ограничение: другое flang/proof/checker/tests/families/restriction/f09-restricted.flang flang/proof/checker/tests/families/restriction/corrupt/other-restriction.record - - - - 1 «1⟩» вместо «0⟩» - - P ограничение: не под «для всех» flang/proof/checker/tests/families/restriction/f09-restricted.flang flang/proof/checker/tests/families/restriction/corrupt/restriction-not-under-the-quantifier.record - - - - 1 стоит не сразу под строкой «для всех» - - @@ -508,6 +508,34 @@ P ограничение: допущение теоремы потеряно fla P ограничение: другое допущение flang/proof/checker/tests/families/restriction/k2bk-theorem-such-that.flang flang/proof/checker/tests/families/restriction/corrupt/other-assumption.record - - - - 1 допущение 1 — в записи ⟨н больше 1⟩ - - P ограничение: гипотеза «дано н больше 0» без строки допущения flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.flang flang/proof/checker/tests/families/restriction/corrupt/hypothesis-without-assumption-line.record - - - - 1 допущение 16 - - say - - - - - - - - - - +say ── семья «гипотеза»: гипотеза теоремы снята ограничением утверждения ── - - - - - - - - - - +C гипотеза: часть «таких что» утверждения (честная) flang/proof/probes/syllogism/assumptions/programs/socrates.flang flang/proof/checker/tests/families/hypothesis/statement-carries-the-hypothesis.record - - - - 0 - - - +P гипотеза: у утверждения «таких что» нет flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-theorem.flang flang/proof/checker/tests/families/hypothesis/statement-does-not-carry-the-hypothesis.record - - - - 1 не является допущением утверждения - - +C гипотеза: предусловие «требует» функции (честная) flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.record - - - - 3 - - - +P гипотеза: предусловие говорит о другом flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.record - - - - 1 не является допущением утверждения - - +C гипотеза: «не меньше 0» из объявленного отрезка (честная) flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.record - - - - 3 - - - +P гипотеза: «не меньше 0» о целом flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.record - - - - 1 не является допущением утверждения - - +say ── вывод из посылок утверждения: шаг «по предположению» проигрывается из «таких что» ── - - - - - - - - - - +C посылки: только в «таких что» утверждения (честная) flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-statement.flang flang/proof/checker/tests/families/assumption-replay/premises-only-in-the-statement.record - - - - 0 - - - +C посылки: Barbara, промежуточный шаг модусом поненсом (честная) flang/proof/probes/syllogism/assumptions/programs/barbara.flang flang/proof/checker/tests/families/assumption-replay/barbara.record - - - - 0 - - - +C посылки: Celarent, поненс к отрицанию (честная) flang/proof/probes/syllogism/assumptions/programs/celarent.flang flang/proof/checker/tests/families/assumption-replay/celarent.record - - - - 0 - - - +C посылки: Darii, цель-конъюнкция (честная) flang/proof/probes/syllogism/assumptions/programs/darii.flang flang/proof/checker/tests/families/assumption-replay/darii.record - - - - 0 - - - +C посылки: Ferio, конъюнкция с отрицанием (честная) flang/proof/probes/syllogism/assumptions/programs/ferio.flang flang/proof/checker/tests/families/assumption-replay/ferio.record - - - - 0 - - - +C посылки: охрана о названном предмете из двух (честная) flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.record - - - - 0 - - - +C посылки: свидетель «есть такой … а именно» (честная) flang/proof/probes/syllogism/assumptions/programs/darii-with-the-existence-word.flang flang/proof/checker/tests/families/assumption-replay/darii-with-the-existence-word.record - - - - 0 - - - +C посылки: Camestres опровержением, цель «нет» (честная) flang/proof/probes/syllogism/assumptions/programs/camestres-by-refutation.flang flang/proof/checker/tests/families/assumption-replay/camestres-by-refutation.record - - - - 0 - - - +P посылки: подтверждение следствия flang/proof/probes/syllogism/assumptions/programs/affirming-the-consequent.flang flang/proof/checker/tests/families/assumption-replay/affirming-the-consequent.record - - - - 1 из посылок утверждения не следует - - +P посылки: нераспределённый средний flang/proof/probes/syllogism/assumptions/programs/undistributed-middle.flang flang/proof/checker/tests/families/assumption-replay/undistributed-middle.record - - - - 1 из посылок утверждения не следует - - +P посылки: незаконное обращение flang/proof/probes/syllogism/assumptions/programs/illicit-conversion.flang flang/proof/checker/tests/families/assumption-replay/illicit-conversion.record - - - - 1 из посылок утверждения не следует - - +P посылки: отрицание антецедента flang/proof/probes/syllogism/assumptions/programs/denying-the-antecedent.flang flang/proof/checker/tests/families/assumption-replay/denying-the-antecedent.record - - - - 1 из посылок утверждения не следует - - +P посылки: экзистенциальный импорт flang/proof/probes/syllogism/assumptions/programs/existential-import.flang flang/proof/checker/tests/families/assumption-replay/existential-import.record - - - - 1 из посылок утверждения не следует - - +P посылки: охрана о другом предмете flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.record - - - - 1 из посылок утверждения не следует - - +P посылки: свидетель, о котором посылок нет flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang flang/proof/checker/tests/families/assumption-replay/witness-without-premises.record - - - - 1 из посылок утверждения не следует - - +P посылки: у теоремы другой свидетель, чем у утверждения flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.flang flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.record - - - - 1 доказывается не то, что обещано - - +P посылки: опровержение без малой посылки flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.flang flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.record - - - - 1 из посылок утверждения не следует - - +P посылки: допущение записи подменено другой посылкой flang/proof/probes/syllogism/assumptions/programs/barbara.flang flang/proof/checker/tests/families/assumption-replay/barbara.record - s/допущение ⟨«всякий».«грек»⟩/допущение ⟨«всякий».«человек»⟩/ - - 1 допущение 3 - - +P посылки: два звена поненса одним шагом — третий исход, не приёмка flang/proof/probes/syllogism/assumptions/programs/barbara-without-the-middle-step.flang flang/proof/checker/tests/families/assumption-replay/barbara-without-the-middle-step.record - - - - 3 - - - +say - - - - - - - - - - say ── семья «утверждение» (ADR-0026 К3a): утверждение без функции ── - - - - - - - - - - C утверждение: связывание и теорема по индукции (честная, проиграна целиком — К3b) flang/proof/checker/tests/families/statement/f05k-statement.flang flang/proof/checker/tests/families/statement/f05k-statement.record - - - - 0 - - - C утверждение: связывание с «таких что» (честная, проиграна целиком — К3b) flang/proof/checker/tests/families/statement/statement-with-restriction.flang flang/proof/checker/tests/families/statement/statement-with-restriction.record - - - - 0 - - - diff --git a/flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-postcondition.record b/flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-postcondition.record new file mode 100644 index 000000000..6e06bf49e --- /dev/null +++ b/flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-postcondition.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang +строк 18 +знаков 397 +отпечаток 532831252 749675408 +ядро 2 +утверждений 1 +отпечаток256 6a99a14564c6c03d2326a43bcffb44ffad8957f916db604b9853dcaf0bd822cb +тотальностей 1 +утверждение «результат положителен» функции «Тождество» строка 6 + вид postcondition + вердикт доказано + теорема «результат положителен» строка 12 + дано «н» строка 13 + допущение ⟨н больше 0⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Тождество» строка 3 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-statement.record b/flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-statement.record new file mode 100644 index 000000000..b78dfdc35 --- /dev/null +++ b/flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-statement.record @@ -0,0 +1,23 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-theorem.flang +строк 17 +знаков 366 +отпечаток 53964851 273723984 +ядро 2 +утверждений 1 +отпечаток256 861637269d91bffa21c869b2793bf0a4c52406d3f2bab7804e55e85f1708e310 + +утверждение «Сократ смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + вердикт доказано + теорема «Сократ смертен» строка 11 + дано «Сократ» строка 12 + допущение ⟨если «Сократ».«человек» то «Сократ».«смертен» иначе да⟩ строка 13 + допущение ⟨«Сократ».«человек»⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 2 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/forgeries/manifest.tsv b/flang/proof/forgeries/manifest.tsv index 2eb94f32d..e16aa9aff 100644 --- a/flang/proof/forgeries/manifest.tsv +++ b/flang/proof/forgeries/manifest.tsv @@ -35,3 +35,5 @@ flang/proof/checker/tests/families/carrier/alias-not-a-segment.flang flang/proof flang/proof/examples/forgery-subtraction-under-precondition.flang flang/proof/checker/tests/records/corpus/poddelka-raznost-bez-poryadka.record record-lies flang/proof/checker/tests/programs/audit-2844/unfold2-itself.flang flang/proof/checker/tests/records/corpus/poddelka-razv2-sebya.record record-lies flang/proof/checker/tests/programs/audit-2844/unfold3-difference.flang flang/proof/checker/tests/records/corpus/poddelka-razv3-raznost.record record-lies +flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-theorem.flang flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-statement.record record-lies +flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-postcondition.record record-lies diff --git a/flang/proof/probes/syllogism/assumptions/expected.tsv b/flang/proof/probes/syllogism/assumptions/expected.tsv index 7b26e0bd2..a7c44c51e 100644 --- a/flang/proof/probes/syllogism/assumptions/expected.tsv +++ b/flang/proof/probes/syllogism/assumptions/expected.tsv @@ -1,16 +1,16 @@ program judge code word socrates.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -socrates.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +socrates.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником barbara.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -barbara.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +barbara.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником celarent.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -celarent.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +celarent.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником darii.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -darii.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +darii.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником ferio.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -ferio.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +ferio.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником camestres-by-refutation.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -camestres-by-refutation.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +camestres-by-refutation.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником socrates-without-a-theorem.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 socrates-without-a-theorem.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику socrates-with-predicates-as-functions.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 @@ -23,8 +23,9 @@ illicit-conversion.flang kernel 1 цель не выведена из допущ existential-import.flang kernel 1 цель не выведена из допущений теоремы denying-the-antecedent.flang kernel 1 цель не выведена из допущений теоремы darii-with-the-existence-word.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -darii-with-the-existence-word.flang checker 1 доказывается не то, что обещано +darii-with-the-existence-word.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником socrates-with-premises-only-in-the-statement.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -socrates-with-premises-only-in-the-statement.flang checker 1 а допущений в записи 0 +socrates-with-premises-only-in-the-statement.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником socrates-with-premises-only-in-the-theorem.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -socrates-with-premises-only-in-the-theorem.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +socrates-with-premises-only-in-the-theorem.flang checker 1 не является допущением утверждения +postcondition-with-a-hypothesis-only-in-the-theorem.flang checker 1 не является допущением утверждения diff --git a/flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang b/flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang new file mode 100644 index 000000000..ffa868935 --- /dev/null +++ b/flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang @@ -0,0 +1,17 @@ +модуль «Reasoning» + +тотальная функция «Тождество» + принимает н: неотрицательное + возвращает неотрицательное + обеспечивает «результат положителен» результат больше 0 + пример «Единица остаётся единицей» + дано н равно 1 + ожидается 1 + н + +теорема «результат положителен» + дано н: неотрицательное + дано н больше 0 + утверждаем результат больше 0 + по предположению + следовательно доказано diff --git a/flang/proof/ratchets.txt b/flang/proof/ratchets.txt index c8441a3e8..319467dad 100644 --- a/flang/proof/ratchets.txt +++ b/flang/proof/ratchets.txt @@ -1,7 +1,7 @@ -forgeries 36 +forgeries 38 forgery-numerator 155 -forgery-probes 611 -checker-code-lines 7949 +forgery-probes 628 +checker-code-lines 8086 checker-primitives 15 trap-kinds 38 trap-goals-on-kernel-word 3 diff --git a/flang/scripts/count-guard.mjs b/flang/scripts/count-guard.mjs index eea378f79..aab358cbb 100644 --- a/flang/scripts/count-guard.mjs +++ b/flang/scripts/count-guard.mjs @@ -43,8 +43,8 @@ * * • ЧИСЛО ФАЙЛОВ он не сверяет. «AST всех 60 файлов `.flang` репозитория * напечатан до и после правки» — не утверждение о размере дерева, а запись о - * том, что ПОКРЫЛ прошлый прогон. Дерево с тех пор выросло до 1087 файла, но - * СНЯТО 2026-10-02 файлов *.flang = 1087 + * том, что ПОКРЫЛ прошлый прогон. Дерево с тех пор выросло до 1097 файла, но + * СНЯТО 2026-10-02 файлов *.flang = 1097 * прогон-то был на шестидесяти, и подставить туда 168 значило бы соврать про * работу, которой не делали. Отличить «столько в дереве» от «столько прошло * через прогон» нечем, кроме чтения, — значит сторож сюда не лезет. diff --git a/flang/scripts/name-guard.mjs b/flang/scripts/name-guard.mjs index 5fe01c06c..faea2fbd3 100644 --- a/flang/scripts/name-guard.mjs +++ b/flang/scripts/name-guard.mjs @@ -130,8 +130,8 @@ * переставшая сравнивать, продолжает зеленеть. * * Поэтому охват ПЕЧАТАЕТСЯ каждым прогоном и закреплён тестом «охват сторожа - * назван числом»: 300 файлов из 1087. Остальные 1099 — не упущение: - * СНЯТО 2026-10-02 файлов *.flang = 1087 + * назван числом»: 300 файлов из 1097. Остальные 1099 — не упущение: + * СНЯТО 2026-10-02 файлов *.flang = 1097 * * • 503 — печать замеров (`docs/benchmark*`): * это ВЫВОД прогона, а не исходник, и правилам имени он не подчиняется; diff --git a/scripts/ledgers/proved-share-ledger.txt b/scripts/ledgers/proved-share-ledger.txt index 02e6cd75a..2c4fefca2 100644 --- a/scripts/ledgers/proved-share-ledger.txt +++ b/scripts/ledgers/proved-share-ledger.txt @@ -1185,6 +1185,15 @@ c895d96922efd9cd69238c4e9fd31b2d|1|1|0|0|0|flang/proof/checker/tests/families/ca f156b44ebb9d062276fb048d8d558551|1|×|×|×|0|flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.flang 43516f88b43387599d936a2979af66d1|1|×|×|×|0|flang/proof/checker/tests/families/restriction/k2bk-theorem-such-that.flang bc17b199769f3c2a966e71d18ebcee89|1|×|×|×|0|flang/proof/checker/tests/families/restriction/f09-restricted.flang +2f70a5cf8cbb44e1a88bdf15eee9b1c9|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang +2c28f2fe75e00f19601f9f6cf9f8d835|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang +ad3459ff6037a5f4fd987dad04cdcb69|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang +d645f02d887cf92fdffc69f02adc2e82|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang +de163bbb2705bdc26ea11008727e938e|1|0|0|0|0|flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang +08921be621f8063b40b5d008e7b9cc08|1|1|0|0|0|flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang +0778794de6b21c38a64ab3059d3d4a6b|1|0|0|0|0|flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.flang +2458efdedb09ab492f1fa9dd4f464080|1|0|0|0|0|flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.flang +5bbe66b669213e9529c7b2d537397100|1|0|0|0|0|flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang 48fabdcaa9d040986fe87d584786ff9b|1|0|0|0|1|flang/proof/checker/tests/families/plan/temporary-directory.flang 58695c0261bca20c054c8f8e7fade6c3|1|0|0|0|1|flang/proof/checker/tests/families/plan/corrupt/foreign-order.flang 441a75abee9f78ef507959ee1b7155a8|1|×|×|×|1|flang/proof/checker/tests/families/coverage/o9-fold-start-one.flang @@ -1598,6 +1607,7 @@ af7fda1d841676c09ef8c20595636892|1|1|0|1|0|flang/proof/checker/tests/programs/75 b84a0d9b2c597e85945650941c5bb1c9|1|0|1|0|0|flang/proof/probes/run/programs/grid.flang 1e489b4612bc356f4c6a28b0b7bfaa4b|1|1|0|1|0|flang/proof/checker/tests/programs/7563/identity.flang 66a842f08485d3ff08202a087187e3b5|1|0|0|0|0|flang/proof/probes/run/programs/plan-proved.flang +fd9c112a1fec91f46377a3ae4c907af2|1|×|×|×|0|flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang 4704717d9ed5ce08f447c0e69f5c6b5f|1|1|0|1|0|flang/proof/checker/tests/programs/7563/unfold1-constructor.flang // ── Набор проб строгого режима (задача 5502), снято 19 сентября 2026 ────── // Семь программ каталога `flang/proof/probes/strict/programs/`; восьмая