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

Typo fix in book

Browse source
This commit is contained in:
Adam Chlipala 2017-04-18 21:01:12 -04:00
parent 9928399f5c
commit a6624bdcf2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
frap_book.tex
View file

@ -3277,7 +3277,7 @@ $$\infer{\hoare{P}{\ifte{b}{c_1}{c_2}}{\lambda s. \; Q_1(s) \lor Q_2(s)}}{
& \hoare{\lambda s. \; P(s) \land \neg \denote{b}(s)}{c_2}{Q_2}
}$$
Coming to loops, we at least have a purpose for the assertion annotated on each one.
Coming to loops, we at last have a purpose for the assertion annotated on each one.
\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 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.