Questions tagged [hoare-logic]
Questions about Hoare's logical framework for program correctness proofs and variants.
11
questions
6
votes
1
answer
1k
views
Question about the formal proof of the inorder traversing
In Don Knuth's famous series of books, The Art of Computer Programming, section 2.3.1, he describes an algorithm to traverse binary tree in inorder, making use of an auxiliary stack:
T1 [Initialize.] ...
- 621
5
votes
3
answers
1k
views
Hoare triple for assignment P{x/E} x:=E {P}
I am trying to understand Hoare logic presented at Wikipedia,
Hoare logic at Wikipedia
Apparently, if I understand correctly, a Hoare triple $$\{P\}~ C ~\{Q\}$$ means
if P just before C, then Q ...
- 374
4
votes
1
answer
113
views
Developing invariants for comparing two strings
The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string):
...
- 9,501
4
votes
2
answers
181
views
The difference between a Hoare Triple/Assertion and a Typed Function
I have been trying to wrap my head around applying Hoare Logic and am running into the question of how Hoare triples are any different from (simply) a typed function.
That is, say you have a typed ...
- 2,163
4
votes
1
answer
1k
views
How to find loop invariant from weakest precondition?
Consider this code:
Precondition:
Postcondition: rv == i <==> ∃i, 0 ≤ i ≤ a.length-1, a[i] == key
...
- 421
2
votes
0
answers
234
views
How to show equivalence of the Hoare assignment axiom vs Floyd assignment axiom?
I know from several sources that they are equivalent, but couldn't find a reasonable explanation. My first approach was to show their equivalence by using the logical consequence rule and both axioms, ...
- 143
2
votes
1
answer
314
views
Understanding Hoare Logic Axioms
Given these 5 axioms of Hoare Logic:
\begin{array}{cl}
\frac{}{\{\phi([x \leftarrow E])\}\ x := E\ \{\phi(x)\}} & \mathtt{Assignment}\\\\
\frac{\{\phi\}\ P_1\ \{\eta\} \quad \{\eta\}\ P_2\ \{\psi\...
- 2,163
1
vote
0
answers
168
views
How to apply Hoare Logic to this function
I would like to apply Hoare Logic to realistic, complex imperative programs that use while loops, if statements, functions, modules, etc. and have side effects (e.g. access the network). In order to ...
- 2,163
1
vote
1
answer
266
views
How to use Hoare Logic to Prove this Assertion
Given this assertion in Hoare Logic:
\begin{align}
&\mathbf{\{p >= 0\}}\\
&s = 0 ; n = 1 ;\\
&\mathtt{while}\ (n <= p)\ \{\\
&\quad s = s + n ;\\
&\quad n = n + 1\\
&\}\\...
- 2,163
1
vote
1
answer
184
views
How to prove $c = a + b$ using Program Verification Techniques
I am trying to prove an elementary thing, but it seems at some point you get down to atoms where you can't prove anything else. This is why I am wondering about proving $c = a + b$, it seems like an ...
- 2,163
1
vote
2
answers
107
views
How to prove a side effect in a function
I asked a question earlier about Saving to the Database, which was very general and about the requirements for a proof when you go through many layers of non-verified systems such as the network and ...
- 2,163