Теормин-ФСВП, страница 3

The UPDATE? flag controls whether update-applications areconverted into IF-THEN-ELSE form and lifted. IF-lifting is the transformation that takes f(IF ATHEN b ELSE c ENDIF) to (IF A THEN f(b) ELSE f(c) ENDIF). LIFT-IF only lifts the leftmostinnermost contiguous block of conditionals so it mighthave to be applied repeatedly to lift all the conditionals. E.g., (lift-if) : applies IF-lifting toevery sequent formula. (lift-if - :updates? nil) : lifts only antecedent IF that are notapplications of updates.expand-- раскрывает по определению n вхождений имени в формуле fnum.

Поумолчанию -- все во всех.(expand “name” [fnum] [n])Expands (and simplifies) the definition of FUNCTION-NAME at a given OCCURRENCE. If noOCCURRENCE is given, then all instances of the definition are expanded. The OCCURRENCEis given as a number n referring to the nth occurrence of the function symbol counting fromthe left, or as a list of such numbers. If the IF-SIMPLIFIES flag is T, then any definitionexpansion occurs only if the RHS instance simplifies (using the decision procedures). Notethat the EXPAND step also applies simplification with decision procedures (i.e. SIMPLIFY withdefault options) to any sequent formulas where an expansion has occurred.

ASSERT? can beeither NONE (meaning no simplification), NIL (meaning simplify using SIMPLIFY), or T(meaning simplify using ASSERT).induct-- выполняет математическую индукцию по переменной дляконсеквента вида FORALL (..., n:nat, ...): P(n). Разбивает доказательство на 2:доказательство базы(в консеквенты добавляется P(0)) и доказательство индуктивногошага(в антецеденты добавляется P(k), в консеквенты -- P(k+1)). Если форолл состоитиз нескольких переменных, наверное, остальные переменные остаются вместе сфоролломsimplify-- простейшие упрощенияФлойдИндуктивное утверждение — для каждой точки сечения — характеризует утверждения между переменнымипри прохождении этой связки.Рецепт: это булевские выражения над переменными x и y.А5. Что из перечисленного может быть оценочной функцией?Рецепт: то что является функцией.

В частности, функцией, возвращающей булево значение (считаем, Boolвырожденным случаем фундированного множества)А6. Что из перечисленного может быть фундированным множеством?Рецепт: пара вида (множество, отношение). Множество -- частично упорядоченное, ограниченное снизу. Этоот отношения зависит. если > то сверху. Левая ж ассоциативность.Частично-упорядоченным множеством ( W, ℏ ) называется непустое множество W и любое бинарноеотношение на этом множестве, которое удовлетворяет следующим свойствам:1. all a, b, c in W :- ( a ℏ b ) /\ ( b ℏ c ) ⇒ a ℏ c [Транзитивность]2.

all a, b in W :- ( a ℏ b ) ⇒ ¬( b ℏ a ) [Асиметричность]3. all a in W :- ¬( a ℏ a ) [Иррефлексивность]Частично-упорядоченное множество ( W, ℏ ) называется фундированным, если не существует бесконечноубывающей последовательности его элементов a0 ℏ a1 ℏ a2 ℏ ….А7. Что из перечисленного может быть условием корректности?Рецепт: Условия корректности определения оценочной функции: all x in Dx, all y in Dy [ qi(x, y) ⇒ ui(x, y) in W]А8. Что из перечисленного может быть условием верификации ?Рецепт: условия верификации: all x in Dx, all y in Dy [ pi(x, y) /\ R(x, y) ⇒ pj( x, r(x, y) ) ]А9.

Что из перечисленного может быть условием завершимости ?Рецепт: условия завершимости: all x in Dx all y in Dy [ qi(x, y) /\ R(x, y) ⇒ ( ui(x,y) > uj(x, r(x, y) ) ) ].Оценочная функция должна убывать.Рецепт: Выбранное множество точек сечения должно быть таким, чтобы каждый цикл в блок-схеме содержал,по крайней мере, одну точку сечения. Одна точка на любое вол-во вложенных уровней. Расположена как вответе. Или если цикл 1 - перед ним.Рецепт:Пусть программа задана своей моделью в виде блок-схемы P, а ее спецификация Ф -- предикатами φ(пре) иψ(пост), тогда:• программа P частично корректна относительно φ и ψ, если для любого векторазначений входных переменных σ, такого что φ(σ) и M[P](σ) ≠ ω выполнено ограничениеψ( σ, M[P](σ) ).

Частичную корректность программы P относительно φ и ψ мы будемобозначать {φ}P{ψ}.• программа P полностью корректна относительно φ и ψ, если для любого векторазначений входных переменных σ, такого что φ(σ) выполнены ограничения M[P](σ) ≠ ω иψ( σ, M[P](σ) ). Полную корректность программы P относительно φ и ψ мы будемобозначать ⟨φ⟩P⟨ψ⟩.Стили спецификаций.По наличию модели состояния:– алгебраический стиль (нет модели) (или, что то же самое, интерфейсная спецификация) В аксиоматическомаксиомы могут иметь произвольный вид, а в алгебраическом это должны быть цепочки термов.– модельный стиль (есть модель)Алгебраическая — интерфейсы системы. Алгебраическая аксиома — пара программ, которые должны даватьодинаковый эффект. (в алгебраической обязаны быть аксиомы)По наличию в спецификации памяти:– аппликативные (нет памяти)– императивные (есть память)Насколько я понял, аппликативные похожи на функциональное программирование (не должно бытьпеременных), императивные, очевидно, на императивное (обязаны быть пременные, то есть память).По виду свойств:– явные (все свойства — эквивалентности)– неявные (свойства — предикаты произвольного вида )value x:axiom xvalue x:axiom xIntis 1Int>0— явное описание— неявное описаниеПолная спецификация — такая, в которой аксиом хватает для вычисления обсерверов.Чтобы вычисление сходилось, длина терма должна уменьшаться с каждым преобразованием по аксиомам.Спецификация, вообще говоря, должна быть неполной — для повышения уровня абстракции и нарочитомигнорировании деталей..