Domácí úkoly 4:

Poznámka: K řešení těchto úkolů je potřeba mít ve stejném adresáři uložené a zkompilované následující soubory s implementací programovacího jazyka Imp a Hoareovy logiky: hoare/LibMaps.v, hoare/LibImp.v, hoare/LibAssertion.v, hoare/LibHoare.v, hoare/LibHoare2.v. Tyto soubory jsou k dispozici na webových stránkách předmětu IADKP.

Příklad A: 1 bod

Připomeňme, že zápis n! označuje faktoriál čísla n (tj. n! = 1*2*...*n]). Ve standardní knihovně Coqu je funkce faktoriál formálně definována pomocí rekurze následujícím způsobem:

    Fixpoint fact (n : nat) : nat :=
      match n with
      | O => 1
      | S n' => S n' * (fact n')
      end.

Uvažujme následující implementaci funkce pro výpočet faktoriálu v jazyce Imp. V dané funkci obsahuje na začátku proměnná X hodnotu n. Po skončení výpočtu by měla proměnná Y obsahovat hodnotu n! (tj. faktoriál n). V daném kódu místo ZDE_DOPLNIT doplňte příslušné anotace tak, abyste následně mohli dokázat korektnost tohoto programu pomocí taktiky verify. Pozn.: Po použití taktiky verify vám zřejmě zbude několik málo nedokázaných tvrzení, která se pravděpodobně budou týkat především nějakých matematických vlastností funkce fact. Pro dokončení důkazu tedy musíte dokázat i tato tvrzení. Připomeňme ještě, že pro volání funkcí Coqu v assertions (jako třeba funkce fact) je třeba použít pomocný operátor ap (nebo ap2 pro binární funkce).

☐

Příklad B: 2 body

Uvažujme následující definici funkce pro výpočet faktoriálu. Podobně jako v předchozím příkladě doplňte v kódu příslušné anotace a dokažte, že tato funkce je korektní. Nápověda: Obecně může být při dokazování tvrzení, která se týkají aritmetických operací na přirozených číslech, jednodušší se vyhnout operacím jako je dělení a místo toho formulovat příslušná tvrzení tak, aby používala jen násobení a další jednoduché operace jako třeba sčítání.

☐

Příklad C: 1 bod

Fibonacciho funkce je obvykle zapsána následujícím způsobem:

      Fixpoint fib n :=
        match n with
        | 0 => 1
        | 1 => 1
        | _ => fib (pred n) + fib (pred (pred n))
        end.

Tato definice neprojde kontrolou Coqu, která ověřuje, že se výpočet této funkce po konečném počtu kroků zastaví. Následující mírně komplikovanější definice touto kontrolou projde.

Dokažte, že funkce fib splňuje následující rovnost. Je možné, že tato rovnost se vám bude hodit při vytváření důkazu v následujícím příkladě.

☐

Příklad D: 2 body

Následující program v jazyce Imp spočítá hodnotu fib n. Tato hodnota by se měla po skončení výpočtu nacházet v proměnné Y. Doplňte anotace v následující definici dfib a dokažte, že splňuje následující specifikaci:

      {{ True }} dfib {{ Y = fib n }}

Pozn.: Pravděpodobně budete potřebovat ve vašich anotacích mnohokrát použít ap.

☐

Příklad E: 4 body

V Hoareově logice můžeme používat několik různých variant pravidel pro přiřazení. Níže jsou uvedeny tři takové varianty označené hoare_assign_A, hoare_assign_B a hoare_assign_C. Dokažte, že všechna tři tato pravidla jsou mezi sebou navzájem odvoditelná, a to bez ohledu na to, jak konkrétně je nadefinován přesný význam Hoareovy trojice. Z toho důvodu je v tomto případě místo hoare_triple použita v daných pravidlech hoare_triple_abstract, o které nic bližšího nepředpokládáme. Kromě toho můžete v důkazech používat pravidla hoare_consequence_pre, hoare_consequence_post a hoare_exists_pre, která zde bereme jako axiomy. Při dokazování se vám mohou hodit rovněž tvrzení t_update_eq, t_update_shadow a t_update_same ze souboru LibMaps.v a případně též následující pomocné tvrzení t_update_restore, které si rovněž dokažte.

☐