(* ***************************************************************** *)
(* *)
(* Released: 2021/04/21. *)
(* Due: 2021/04/25, 23:59:59, CST. *)
(* *)
(* 0. Read instructions carefully before start writing your answer. *)
(* *)
(* 1. You should not add any hypotheses in this assignment. *)
(* Necessary ones have been provided for you. *)
(* *)
(* 2. In order to check whether you have finished all tasks or not, *)
(* just see whether all "Admitted" has been replaced. *)
(* *)
(* 3. You should submit this file (Assignment6a.v) on CANVAS. *)
(* *)
(* 4. Only valid Coq files are accepted. In other words, please *)
(* make sure that your file does not generate a Coq error. A *)
(* way to check that is: click "compile buffer" for this file *)
(* and see whether an "Assignment6a.vo" file is generated. *)
(* *)
(* 5. Do not copy and paste others' answer. *)
(* *)
(* 6. Using any theorems and/or tactics provided by Coq's standard *)
(* library is allowed in this assignment, if not specified. *)
(* *)
(* 7. When you finish, answer the following question: *)
(* *)
(* Who did you discuss with when finishing this *)
(* assignment? Your answer to this question will *)
(* NOT affect your grade. *)
(* (* FILL IN YOUR ANSWER HERE AS COMMENT *) *)
(* *)
(* ***************************************************************** *)
Require Import PL.Imp.
Require Import Coq.Lists.List.
Import ListNotations.
Import Assertion_D.
Import Abstract_Pretty_Printing.
(* ################################################################# *)
(** * Task 1: Understanding Weakest Preconditions *)
Module Task1.
(** **** Exercise: 3 stars, standard *)
(** Which of the following statements about weakest preconditions are correct?
- 1. For any assertion [P], program variable [X] and integer expression [E],
[ P [X |-> E] ] is a weakest precondition of [X ::= E] and [P].
- 2. For any assertion [P], logical variable [x], program variable [X] and
integer expression [E], if [x] does not freely occur in [P], then [ P ] is
a weakest precondition of [X ::= E] and
[ EXISTS x, P [X |-> x] AND {[ X ]} = {[ E [X |-> x] ]} ].
- 3. If [P] is a weakest precondition of [c] and [Q], and [P] is equivalent
to [P'], then [P'] is also a weakest precondition of [c] and [Q]. (Here,
we say that [P] and [P'] are equivalent when: for any interpretation [J],
[J |== P] if and only if [J |== P'].)
This is a multiple-choice problem. You should use an ascending Coq list to
describe your answer, e.g. [1; 2; 3], [1; 3], [2]. *)
Definition my_choice1: list Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(** **** Exercise: 3 stars, standard *)
(** Which of the following statements about weakest preconditions are correct?
- 1. [True] is a weakest precondition of [While (X <= X) Do Skip EndWhile]
and [False].
- 2. [False] is a weakest precondition of [While (X <= X) Do Skip EndWhile]
and [False].
- 3. For any assertions [P], [Q], any boolean expression [b] and any loop
body [c], if [P] is a weakest precondition of [While b Do c EndWhile] and
[Q], and [P] is also a weakest precondition of [While b Do c EndWhile] and
[ P AND NOT {[ b ]} ].
This is a multiple-choice problem. You should use an ascending Coq list to
describe your answer, e.g. [1; 2; 3], [1; 3], [2]. *)
Definition my_choice2: list Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
End Task1.
(* ################################################################# *)
(** * Task 2: Understanding VST *)
Module Task2.
(** **** Exercise: 1 star, standard *)
(** In our tutorial, we cannot prove that the following C program satisfying
the Hoare triple below.
int add(int x, int y) {
int z;
z = x + y;
return z;
}
Definition add_spec :=
DECLARE _add
WITH x: Z, y: Z
PRE [ tint, tint ]
PROP ()
PARAMS (Vint (Int.repr x); Vint (Int.repr y))
GLOBALS ()
SEP ()
POST [ tint ]
PROP ()
RETURN (Vint (Int.repr (x + y)))
SEP ().
The reason is that overflow in signed integer arithmetic is undefined
behavior in C and the precondition does not exclude that possibility.
Is the explanation above correct? 1. Yes. 2. No. *)
Definition my_choice1: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(** **** Exercise: 1 star, standard *)
(** In VST, [forward] is a powerful command for forward symbolic execution. For
example, the following is to one proof goal before [forward] and the
corresponding proof goal after [forward].
[
semax Delta
(PROP ( )
LOCAL (temp _w w;
temp _v v)
SEP (listrep s1 w;
data_at Tsh t_struct_list (Vint (Int.repr s2a), y) v;
listrep s2b y))
(_t = (_v -> _tail);
MORE_COMMANDS)
POSTCONDITION
]
[
semax Delta
(PROP ( )
LOCAL (temp _t y;
temp _w w;
temp _v v)
SEP (listrep s1 w;
data_at Tsh t_struct_list (Vint (Int.repr s2a), y) v;
listrep s2b y))
((_v -> _tail) = _w;
MORE_COMMANDS)
POSTCONDITION
]
The [forward] tactic actually builds a Hoare logic proof tree for the former
triple from a proof tree for the latter triple. In this proof, it uses
VST's consequence rule and some other Hoare logic proof rules.
Which of the following proof rules are needed?
1. The assgnment rule.
2. The sequence rule.
3. The assgnment rule and the sequence rule. *)
Definition my_choice2: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(** **** Exercise: 1 star, standard *)
(** Is the following statement correct? 1. Yes. 2. No.
In VST, we can prove the following assertion derivation:
forall p v, data_at Tsh tint v p |--
data_at Tsh tint v p * data_at Tsh tint v p *)
Definition my_choice3: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
End Task2.
(* 2021-04-21 17:20 *)