pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2025-02-26 03:22:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Some ModelChecking improvements

Browse source
This commit is contained in:
Adam Chlipala 2018-03-04 19:23:36 -05:00
parent b0ad93e6a4
commit 712aacf9de
2 changed files with 11 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
ModelChecking.v
View file

@ -173,7 +173,9 @@ Proof.
assumption. assumption.
Qed. Qed.
(* A trivial fact about union and singleton sets. *) (* A trivial fact about union and singleton sets.
* Note that we model sets as functions that are passed elements, deciding in
* each case whether that element belongs to the set. *)
Theorem singleton_in : forall {A} (x : A) rest, Theorem singleton_in : forall {A} (x : A) rest,
({x} \cup rest) x. ({x} \cup rest) x.
Proof. Proof.
@ -264,7 +266,7 @@ Proof.
apply oneStepClosure_empty. apply oneStepClosure_empty.
simplify. simplify.
(* Now the candidate invariatn is closed under single steps. Let's prove (* Now the candidate invariant is closed under single steps. Let's prove
* it. *) * it. *)
apply MscDone. apply MscDone.
apply prove_oneStepClosure; simplify. apply prove_oneStepClosure; simplify.
@ -346,7 +348,9 @@ Ltac model_check := model_check_find_invariant; model_check_finish.
(* END CODE THAT WILL NOT BE EXPLAINED IN DETAIL! *) (* END CODE THAT WILL NOT BE EXPLAINED IN DETAIL! *)
(* Now watch this. We can check various instances of factorial (* Now watch this. We can check various instances of factorial
* automatically. *) * automatically. Notice that reachable states are printed as we encounter them
* in exploration, using [idtac] invocations above. This printing is for the
* user's understanding and has no logical meaning. *)
Theorem factorial_ok_2_snazzy : Theorem factorial_ok_2_snazzy :
invariantFor (factorial_sys 2) (fact_correct 2). invariantFor (factorial_sys 2) (fact_correct 2).
@ -695,7 +699,8 @@ Proof.
(* It finds exactly four reachable states. We finish by showing that they all (* It finds exactly four reachable states. We finish by showing that they all
* obey the original invariant. *) * obey the original invariant. *)
invert 1. invert 1. (* Note that this [1] means "first premise below the double
* line." *)
invert H0. invert H0.
simplify. simplify.
unfold add2_correct. unfold add2_correct.
@ -960,8 +965,7 @@ Proof.
(* We get 7 neat little states, one per program counter. Next, we prove that (* We get 7 neat little states, one per program counter. Next, we prove that
* each of them implies the original invariant. *) * each of them implies the original invariant. *)
invert 1. (* Note that this [1] means "first premise below the double invert 1.
* line." *)
invert H0. invert H0.
unfold loopy_correct. unfold loopy_correct.
simplify. simplify.

2
frap_book.tex
View file

@ -1398,7 +1398,7 @@ For our purposes, the key pay-off from this connection is that we may translate
If $\angled{S, S_0, \to} \simulate_R \angled{S', S'_0, \to'}$, and if $I$ is an invariant of $\angled{S', S'_0, \to'}$, then $R^{-1}(I)$ is an invariant of $\angled{S, S_0, \to}$. If $\angled{S, S_0, \to} \simulate_R \angled{S', S'_0, \to'}$, and if $I$ is an invariant of $\angled{S', S'_0, \to'}$, then $R^{-1}(I)$ is an invariant of $\angled{S, S_0, \to}$.
\end{theorem} \end{theorem}
We can apply this theorem to the two example programs from earlier in the section. We can apply this theorem to the two example programs from earlier in the section, now imagining that we run two parallel-thread copies of each program, using last chapter's approach to modeling threads with transition systems.
The concrete system can be represented with thread-local states $\{\mathsf{Read}\} \cup \{\mathsf{Write}(n) \mid n \in \mathbb N\}$ and the abstract system with $\{\mathsf{BRead}\} \cup \{\mathsf{BWrite}(b) \mid b \in \mathbb B\}$, for the Booleans $\mathbb B$. The concrete system can be represented with thread-local states $\{\mathsf{Read}\} \cup \{\mathsf{Write}(n) \mid n \in \mathbb N\}$ and the abstract system with $\{\mathsf{BRead}\} \cup \{\mathsf{BWrite}(b) \mid b \in \mathbb B\}$, for the Booleans $\mathbb B$.
We define compatibility between local states. We define compatibility between local states.