1. Постройте модель для следующих символов и конъюнкции утверждений:

    function a: int

    function b: int

    function f int int: int

    f a a <> f b b

    f a b = a

    f (f b a) b <> f a b </code>

  2. Определите и докажите наличие/отсутствие логического следствия (при помощи построения модели):

    function z: int

    function d: int

    function f int int: int

    axiom A0: z <> d

    axiom A1: forall a. f z a = a

    axiom A2: forall a b. f a b = f b a

    goal G: forall x. f (f z x) (f x d) = f (f x x) d </code>

  3. Определите и докажите наличие/отсутствие логического следствия (при помощи построения модели) - те же символы, что и в предыдущем задании, но везде вместо int используется множество мощности 2.

  4. Та же задача, что и пункте 2, но с еще одной аксиомой: 
    axiom A3: forall a b c. f (f a b) c = f a (f b c)

  5. Определите всё необходимое для поддержки знаковой машинной арифметики (сложение, вычитание, умножение, сравнения): тип-символ для ограниченных целых, функциональные и предикатные символы, примитивы для моделей программы.

  6. На языке WhyML напишите модель программы и модель требований из практического задания 1. Используйте аксиоматизацию из предыдущего упражнения. Докажите полную корректность.

  7. Определите теорию для списков – последовательностей конечной длины из значений некоторого одного типа.

  8. При помощи наших средств докажите следующее утверждение: длина конкатенации списков равна сумме их длин.