pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising for tomorrow's lecture

Browse source
This commit is contained in:
Adam Chlipala 2022-04-03 14:02:22 -04:00
parent 33733a0450
commit 0e13a0a695
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
frap_book.tex
View file

@ -3916,8 +3916,8 @@ Coming to loops, we at last have a purpose for the assertion annotated on each o
\invariants \invariants
We call those assertions \emph{loop invariants}\index{loop invariants}; one of these is meant to be true every time a loop iteration begins. We call those assertions \emph{loop invariants}\index{loop invariants}; one of these is meant to be true every time a loop iteration begins.
We will try to avoid confusion with the more fundamental concept of invariant for transition systems, though in fact the two are closely related formally, which we will see in the last section of this chapter. We will try to avoid confusion with the more fundamental concept of invariant for transition systems, though in fact the two are closely related formally, which we will see in the last section of this chapter.
Essentially, the loop invariant gives the \emph{induction hypothesis} that makes the program correctness proof go through. Essentially, the loop invariant gives the \emph{induction hypothesis} that makes the program-correctness proof go through.
We encapsulate the induction reasoning once and for all, in the proof of soundness for Hoare triples. We encapsulate the induction reasoning once-and-for-all, in the proof of soundness for Hoare triples.
To verify an individual program, it is only necessary to prove the premises of the rule, which we give now. To verify an individual program, it is only necessary to prove the premises of the rule, which we give now.
$$\infer{\hoare{P}{\{I\} \while{b}{c}}{\lambda s. \; I(s) \land \neg \denote{b}(s)}}{ $$\infer{\hoare{P}{\{I\} \while{b}{c}}{\lambda s. \; I(s) \land \neg \denote{b}(s)}}{
(\forall s. \; P(s) \Rightarrow I(s)) (\forall s. \; P(s) \Rightarrow I(s))
@ -3955,7 +3955,7 @@ Here we only go into detail on a proof of the dual property, \emph{soundness}\in
By induction on the derivation of $\bigstep{(h, v, \{I\} \while{b}{c})}{(h', v')}$. By induction on the derivation of $\bigstep{(h, v, \{I\} \while{b}{c})}{(h', v')}$.
\end{proof} \end{proof}
That lemma encapsulates once and for all the use of induction in reasoning about the many iterations of loops. That lemma encapsulates once-and-for-all the use of induction in reasoning about the many iterations of loops.
\begin{theorem}[Soundness of Hoare logic] \begin{theorem}[Soundness of Hoare logic]
If $\hoare{P}{c}{Q}$, $\bigstep{(h, v, c)}{(h', v')}$, and $P(h, v)$, then $Q(h', v')$. If $\hoare{P}{c}{Q}$, $\bigstep{(h, v, c)}{(h', v')}$, and $P(h, v)$, then $Q(h', v')$.
@ -3973,7 +3973,7 @@ After a step like this one, it is guaranteed that the ``fundamental'' rule now a
This process creates a pile of side conditions to be proved by other means, corresponding to the assertion implications generated by the rules for loops, assertions, and consequence. This process creates a pile of side conditions to be proved by other means, corresponding to the assertion implications generated by the rules for loops, assertions, and consequence.
Many real-world tools based on Hoare logic discharge such goals using solvers for satisfiability modulo theories\index{satisfiability modulo theories}, otherwise known as SMT solvers\index{SMT solvers}. Many real-world tools based on Hoare logic discharge such goals using solvers for satisfiability modulo theories\index{satisfiability modulo theories}, otherwise known as SMT solvers\index{SMT solvers}.
The accompanying Coq code just uses a modest Coq automation tactic definition building on the proof steps we have been using all along. The accompanying Coq code just uses a modest Coq automation-tactic definition building on the proof steps we have been using all along.
It is not complete by any means, but it does surprisingly well in the examples we step through, of low to moderate complexity. It is not complete by any means, but it does surprisingly well in the examples we step through, of low to moderate complexity.
Before closing our discussion of the basics of Hoare logic, let's consider how it brings to bear some more of the general principles that we have met before. Before closing our discussion of the basics of Hoare logic, let's consider how it brings to bear some more of the general principles that we have met before.