Questions tagged [hoare-logic]

Questions about Hoare's logical framework for program correctness proofs and variants.

Filter by
Sorted by
Tagged with
3
votes
1answer
827 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 ...
2
votes
0answers
163 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, ...
4
votes
1answer
89 views

Developing invariants for comparing two strings

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
2
votes
1answer
140 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\...
4
votes
2answers
102 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 ...
1
vote
2answers
51 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 ...
1
vote
0answers
63 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 ...
1
vote
1answer
134 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\\ &\}\\...
1
vote
1answer
76 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 ...