Skip to main content

Questions tagged [hoare-logic]

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

Filter by
Sorted by
Tagged with
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.] ...
Yai0Phah's user avatar
  • 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 ...
zell's user avatar
  • 374
4 votes
2 answers
202 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 ...
Lance's user avatar
  • 2,243
4 votes
1 answer
2k 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 ...
Teodorico Levoff's user avatar
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): ...
hengxin's user avatar
  • 9,561
3 votes
1 answer
176 views

How did this work apply weakest precondition rule on their example car problem?

While reading the example given in [1]., I couldn't understand how the authors set up the logic to compute the weakest preconditions (wp) in their car example in section 4.2. The dynamics of the ...
desert_ranger's user avatar
2 votes
1 answer
345 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\...
Lance's user avatar
  • 2,243
2 votes
0 answers
247 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, ...
Mad A.'s user avatar
  • 143
1 vote
0 answers
178 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 ...
Lance's user avatar
  • 2,243
1 vote
1 answer
280 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\\ &\}\\...
Lance's user avatar
  • 2,243
1 vote
1 answer
199 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 ...
Lance's user avatar
  • 2,243
1 vote
2 answers
116 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 ...
Lance's user avatar
  • 2,243