(** * Domácí úkoly 6: *) (*----------------------------------------------------------------------------*) (** 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. *) (*----------------------------------------------------------------------------*) Require Import LibHoare2. From Stdlib Require Import Bool. From Stdlib Require Import Arith. From Stdlib Require Import EqNat. From Stdlib Require Import PeanoNat. Import Nat. From Stdlib Require Import Lia. Open Scope dcom_scope. Definition ZDE_DOPLNIT := <{True}>. (*----------------------------------------------------------------------------*) (** **** 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ě Rocqu 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í Rocqu v assertions (jako třeba funkce [fact]) je třeba použít pomocný operátor [#]. *) Definition factorial_v1_dec (n:nat) : decorated := <{ {{ X = n }} ==> {{ ZDE_DOPLNIT }} Y := 1 {{ ZDE_DOPLNIT }}; W := 0 {{ ZDE_DOPLNIT }}; while W < X do {{ ZDE_DOPLNIT }} ==> {{ ZDE_DOPLNIT }} W := 1 + W {{ ZDE_DOPLNIT }}; Y := Y * W {{ ZDE_DOPLNIT }} end {{ ZDE_DOPLNIT }} ==> {{ Y = #fact n }} }>. Theorem factorial_v1_correct: forall n, outer_triple_valid (factorial_v1_dec n). Proof. (* ZDE DOPLŇTE DŮKAZ *) Admitted. (** [] *) (*----------------------------------------------------------------------------*) (** **** 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í. *) Definition factorial_v2_dec (n:nat) : decorated := <{ {{ X = n }} ==> {{ ZDE_DOPLNIT }} Y := 1 {{ ZDE_DOPLNIT }} ==> {{ ZDE_DOPLNIT }}; while X > 1 do {{ ZDE_DOPLNIT }} Y := X * Y {{ ZDE_DOPLNIT }}; X := X - 1 {{ ZDE_DOPLNIT }} end {{ ZDE_DOPLNIT }} ==> {{ Y = #fact n }} }>. Theorem factorial_v2_correct: forall n, outer_triple_valid (factorial_v2_dec n). Proof. (* ZDE DOPLŇTE DŮKAZ *) Admitted. (** [] *) (*----------------------------------------------------------------------------*) (** **** 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 Rocqu, 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. *) Fixpoint fib n := match n with | 0 => 1 | S n' => match n' with | 0 => 1 | S n'' => fib n' + fib n'' end end. (** 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ě. *) Lemma fib_eqn : forall n, n > 0 -> fib n + fib (pred n) = fib (1 + n). Proof. (* ZDE DOPLŇTE DŮKAZ *) Admitted. (** [] *) (*----------------------------------------------------------------------------*) (** **** 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 [#]. *) Definition T : var := "T"%string. Definition dfib (n : nat) : decorated := <{ {{ True }} ==> {{ ZDE_DOPLNIT }} X := 1 {{ ZDE_DOPLNIT }}; Y := 1 {{ ZDE_DOPLNIT }}; Z := 1 {{ ZDE_DOPLNIT }}; while X <> 1 + n do {{ ZDE_DOPLNIT }} ==> {{ ZDE_DOPLNIT }} T := Z {{ ZDE_DOPLNIT }}; Z := Z + Y {{ ZDE_DOPLNIT }}; Y := T {{ ZDE_DOPLNIT }}; X := 1 + X {{ ZDE_DOPLNIT }} end {{ ZDE_DOPLNIT }} ==> {{ Y = #fib n }} }>. Theorem dfib_correct : forall n, outer_triple_valid (dfib n). Proof. (* ZDE DOPLŇTE DŮKAZ *) Admitted. (** [] *) (*----------------------------------------------------------------------------*) (** **** 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 [valid_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. *) Lemma t_update_restore (x : var) (v : value) (st : state) : (x !-> st x; x !-> v; st) = st. Proof. (* ZDE DOPLŇTE DŮKAZ *) Admitted. Module Hoare_assign. Parameter hoare_triple_abstract : Assertion -> com -> Assertion -> Prop. Notation "{[ P ]} c {[ Q ]}" := (hoare_triple_abstract P c Q) (at level 2, P custom assn at level 99, c custom com at level 99, Q custom assn at level 99) : hoare_spec_scope. Axiom hoare_consequence_pre : forall P P' Q c, {[ P' ]} c {[ Q ]} -> (P ==> P') -> {[ P ]} c {[ Q ]}. Axiom hoare_consequence_post : forall P Q Q' c, {[ P ]} c {[ Q' ]} -> (Q' ==> Q) -> {[ P ]} c {[ Q ]}. Axiom hoare_exists_pre : forall {M : Type} P Q c, (forall x, {[ $(P x) ]} c {[ Q ]}) -> {[ $(fun st => exists x : M, P x st) ]} c {[ Q ]}. Definition hoare_assign_A := forall P x a, {[ P [x |-> a] ]} <{ x := a }> {[ P ]}. Definition hoare_assign_B := forall x a m P, {[ $(fun st => P st /\ st x = m) ]} <{ x := a }> {[ $(fun st => P (x !-> m ; st) /\ st x = aeval (x !-> m ; st) a) ]}. Definition hoare_assign_C := forall x a P, {[ $(fun st => P st) ]} <{ x := a }> {[ $(fun st => exists m, P (x !-> m ; st) /\ st x = aeval (x !-> m ; st) a) ]}. Theorem B_from_A : hoare_assign_A -> hoare_assign_B. Proof. (* ZDE DOPLŇTE DŮKAZ *) Admitted. Theorem C_from_A : hoare_assign_A -> hoare_assign_C. Proof. (* ZDE DOPLŇTE DŮKAZ *) Admitted. Theorem A_from_B : hoare_assign_B -> hoare_assign_A. Proof. (* ZDE DOPLŇTE DŮKAZ *) Admitted. Theorem A_from_C : hoare_assign_C -> hoare_assign_A. Proof. (* ZDE DOPLŇTE DŮKAZ *) Admitted. End Hoare_assign. (** [] *) (*----------------------------------------------------------------------------*)