Write an Imp program [c] that swaps the values of [X] and [Y] and show that it satisfies the following specification: {{X <= Y}} c {{Y <= X}} Your proof should not need to use [unfold valid_hoare_triple]. Hints: - Remember that Imp commands need to be enclosed in <{...}> brackets. - Remember that the assignment rule works best when it's applied "back to front," from the postcondition to the precondition. So your proof will want to start at the end and work back to the beginning of your program. - Remember that [eapply] is your friend.) *) Definition swap_program : com (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted. Theorem swap_exercise : {{X <= Y}} swap_program {{Y <= X}}. Proof. (* FILL IN HERE *) Admitted. (** [] *)
** **** Exercise: 3 stars, standard (swap_exercise)
Write an Imp
show that it satisfies the following specification:
{{X <= Y}} c {{Y <= X}}
Your proof should not need to use [unfold valid_hoare_triple].
Hints:
- Remember that Imp commands need to be enclosed in <{...}>
brackets.
- Remember that the assignment rule works best when it's
applied "back to front," from the postcondition to the
precondition. So your proof will want to start at the end
and work back to the beginning of your program.
- Remember that [eapply] is your friend.) *)
Definition swap_program : com
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem swap_exercise :
{{X <= Y}}
swap_program
{{Y <= X}}.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
From the book software Foundations Volume 2 coq proof
Step by step
Solved in 3 steps