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
21 votes
1 answer
3k views

Difference between Dependent type , refinement type and Hoare Logic

I know little dependent type theory. From wikipedia : A dependent type is a type whose definition depends on a value. And from my Type theory course i recall that a dependent type is : Family ...
Pushpa's user avatar
  • 933
18 votes
5 answers
6k views

Example of an algorithm that lacks a proof of correctness

We have Hoare logic. Why is it still possible that an algorithm is right but there is no proof that it's correct? Suppose the algorithm is expressed in C. Then we can argue step by step that it's ...
Zirui Wang's user avatar
12 votes
2 answers
2k views

How to deal with arrays during Hoare-style correctness proofs

In the discussion around this question, Gilles mentions correctly that any correctness proof of an algorithm that uses arrays has to prove that there are no out-of-bounds array accesses; depending on ...
Raphael's user avatar
  • 72.6k
8 votes
1 answer
317 views

What was the major breakthrough between Hoare-Floyd logic and Scott–Strachey semantics?

I'm reading through a commentary on Milner's "The use of machines to assist in rigorous proof" by Mike Gordon. In this paper, he explains how LCF was born from the ideas of denotational semantics by ...
user1868607's user avatar
  • 2,194
7 votes
1 answer
381 views

Hoare logic - total correctness of loops

Consider a while loop of the form : $\texttt{while (C) {S}}$ with $\texttt{C}$ the condition and $\texttt{S}$ the body of the loop. Let $\texttt{I}$ and $\texttt{V}$ respectively be an invariant ...
Dory's user avatar
  • 73
6 votes
3 answers
1k views

Intuitive explanation of Hoare assignment axiom

$\small\textit{''The obvious things are the most difficult to understand''}$ May be the question does not make sense, but let me ask it anyway. The Hoare assignment axiom is $$ \dfrac{}{\{Q[v \...
Ayrat's user avatar
  • 1,075
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
5 votes
2 answers
6k views

What does it mean to "strengthen the precondition and weaken the postcondition" in Hoare logic?

Having learned a rough summary of Hoare logic (i.e. learning just the basic concept of Hoare triples and a few of the rules) I kept seeing a statement along these lines: The rule of consquence ...
Dave's user avatar
  • 495
5 votes
1 answer
2k views

What is a predicate transformer?

I'm reading Programming - The derivation of algorithms, and I want to understand the purpose of a predicate transformer. This is the excerpt (p. 14-15): A more precise way in which constructs may be ...
InfZero's user avatar
  • 183
5 votes
1 answer
245 views

Relation between Hoare Type Theory and pointers

My understanding is that in Hoare Type Theory every imperative statement has a type of the form {Pre}res:T{Post} where T is the ...
Pasqui23's user avatar
5 votes
2 answers
782 views

Why is the assignment rule the way it is in Hoare Logic?

Why is the assignment rule the way it is in Hoare Logic/Axiomatic Semantics? I can't wrap my head around why the assignment rule is backwards from what I expected. I understand Hoare logic is use to ...
Charlie Parker's user avatar
5 votes
2 answers
219 views

proving program equivalence

I understand that the general problem of program equivalence is undecidable, but I'm wondering what approaches exist to tackle the problem? I am familiar with Hoare-style verification, but are there ...
user120913's user avatar
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
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
4 votes
1 answer
217 views

Continuation-passing style: what is meant by "CPS'ing"?

I'm reading Dijkstra Monads for Free for a presentation I'll be doing and it's pretty meaty. One of the things that I keep running into is the term "CPS'ing". I've read a little bit on ...
Ben Kushigian's user avatar
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
3 votes
1 answer
611 views

Hoare logic, proving conjunction rule from basic rules, possible or not?

(This is HW.) Suppose I have these following proof rules given. I am currently considering if I can prove the conjunction rule (given below) from the above given Hoare logic rules. My answer would ...
runeblaze's user avatar
  • 189
3 votes
1 answer
545 views

The Law of Excluded Miracle in the language of guarded commands

The definition of weakest precondition is familiar (let me use Isabelle's syntax here): definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t" the weakest precondition ...
user1868607's user avatar
  • 2,194
3 votes
1 answer
411 views

Why precondition strengtening is sound in Hoare logic

I have problem with understanding why precondition strengthening is sound rule in Hoare logic. The rule is: $$ {P \implies Q, \{Q\} C \{X\} } \over {\{P\} C \{X\}} $$ I really do not understand why ...
Trismegistos's user avatar
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
3 votes
1 answer
83 views

What's the meaning of the $\top$ symbol in a Hoare triple?

I'm studying program verification and came across the following triple: $$ \{\top\} \;P \; \{y=(x+1)\} $$ What's the meaning of the $\top$ symbol on the precondition? Does it mean $P$ can take any ...
Fratel's user avatar
  • 43
3 votes
1 answer
43 views

Formal semantics of a mutable/imperative stack

When introducing formal semantics for data structures, immutable stacks are a nice simple example : $\mathit{is\_empty}(\mathit{create()})=\mathrm{True}$ $\mathit{is\_empty}(\mathit{push}(e, s))=\...
ysalmon's user avatar
  • 233
3 votes
0 answers
803 views

Expression of the weakest precondition of a while loop

I am interested in computing weakest preconditions (WP) of loops. If I refer to Wikipedia "Predicate Transformer semantics", the WP for e.g. total correction of a loop annotated with an invariant I ...
Zooky's user avatar
  • 131
3 votes
0 answers
96 views

Spot the formalism (some kind of process logic)

Consider the following specification technique. A specification consists of a finite set of triples $\langle C, A, C' \rangle$, where $A$ is the name of an action and $C, C'$ are conditions, that is, ...
reinierpost's user avatar
  • 5,738
2 votes
1 answer
354 views

Find the loop invariant of the given while loop

I don't know how to find a loop invariant. I'm not sure where to start. Can anyone find the loop invariant of the given program and explain your method please. ...
the_martian's user avatar
2 votes
1 answer
1k views

Proving the loop invariant for a simple program in Hoare logic

I was studying loop invariant and came across Tomas Petricek's example. Here's the equivalent(I believe) program after I revised it a bit for proof in Hoare logic: ...
RexYuan's user avatar
  • 234
2 votes
2 answers
76 views

How to change the algorithm implication by changing the invariant?

I have this specification in GCL: $[Ctx C: n\geqslant 0\ \wedge\ b:[0..n-1]\ \text{of int}$ $\{Q:\text{True}\}$ $sum,i:=0,0;$ $\{\text{Invariant}\ P: 0\leqslant i \leqslant n\ \wedge sum=\sum_{j=0}...
InfZero's user avatar
  • 183
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
1 answer
1k views

Check whether loop invariants are correct?

I'm trying to prove some code is correct, using Hoare logic. How do I check whether my loop invariants are correct? I'm asked to prove (using Hoare Logic) that the following program is valid: ...
Greg Peckory's user avatar
2 votes
1 answer
306 views

Axiomatic Semantics and Postconditions

I'll preface this by saying that this IS a homework question. However, when asked about how to solve it in class, (I believe) my professor was unable to complete it. The question is: Compute the ...
FuriousFolder's user avatar
2 votes
1 answer
49 views

Bottleneck in Hoare Logic unable to arrive at my {P} from {Q}

{Q} = {n>0} C1 = i := 1; C2 = c := 1; C3 = p := 0; {P} = {i<=n, p = fib(i-1), c = fib(i)} My lack of understanding towards the rule of consequence in hoare logic is blocking me from find the ...
Jerry Sui's user avatar
2 votes
1 answer
390 views

Hoare logic - invariant of loop [closed]

I am trying to prove partial corectness of following program: ...
user avatar
2 votes
0 answers
176 views

Hoare triple: Loop invariant and partial correctness

Below there is Hoare triple in which variable $a$ is an array of integers, $len$, $x, i$ are integer-valued variables, and $r$ is a Boolean-valued variable. I have to provide a loop invariant (using ...
BoiD's user avatar
  • 21
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
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
1 vote
1 answer
78 views

what is the 'x :=' part mean in a hoare triple?

In Hoare logic, there's a thing called a Hoare triple, e.g.$$ \begin{array}{ccccc} \{x = 2\} & & x := x+1 & & \{x = 3\} \end{array}. $$ What does '$x :=$' mean?
Tremmer Scott's user avatar
1 vote
1 answer
46 views

Hoare-Logic: Requirements for imperfect data types

Theoretically, Hoare-Logic let's one prove the correctness of an algorithm, given pre- and post-condition. However, as far as I've seen it so far, one idealizes his data-types to a mathematical set ...
Sudix's user avatar
  • 709
1 vote
1 answer
250 views

How to prove the equivalence between Hoare and Floyd assignment axioms?

How to show that these two axioms are equivalent: 1: $\{G[v/e]\} v:=e \{G\}$ 2: $\{F\} v:=e \{\exists v' (F[v/v'] \land v=e[v/v'])\}$ I've tried with $G = \exists v' (F[v/v'] \land v=e[v/v']) $and ...
Martin Matak's user avatar
1 vote
1 answer
95 views

Logic foundation for formal verification

What types of logic should one study as foundation before diving into the area of software verification? What I can think of are: Hoare Logic (for proving correctness of imperative programs) Linear ...
a_fan's user avatar
  • 111
1 vote
1 answer
163 views

How to determine the pre and post conditions of a program (Hoare-logic)

Problem Below is a program named X: y = 1; while(y < x){ y = 10 * y; } What does this program X do? What are appropriate pre and post conditions? (Assume ...
August Jelemson's user avatar
1 vote
1 answer
105 views

How to solve for the precondition give a postcondtion that must satisfy two conditions

I tried solving past exam question but there is this one that I haven't been able to solve. The question states that a suitable precondition should be found for the statement. $$ a= i +2; i++\{(a = ...
Jsph's user avatar
  • 23
1 vote
2 answers
3k views

how to solve Hoare logic problems

I'm having trouble proving Hoare logic questions as I'm not sure of the process that is taken to prove them. I understand that they're rules such as assignment axiom, pre-condition strengthening, post-...
Tremmer Scott's user avatar
1 vote
1 answer
391 views

True Postcondition, with true Precondition

In my exam preparation I stumbled across the follwoing exercise regarding pre and postconditions: As far as I understood the question, we need to express some condition for p, such that if that ...
Stefan's user avatar
  • 45
1 vote
1 answer
268 views

Hoare's Axiom Scheme Precondition

I have a question about determining preconditions for Hoare's Axiom Scheme. For example, if we have P { x=2 } x==1 and we are trying to determine the precondition, ...
James Teller's user avatar
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
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
207 views

Loop termination - Loop invariant

(x >= 0 && y >= 0) q = 0; r = x; while ( r >=y ) { r = r - y; q = q + 1; } (x = q*y +r) && (r >= 0) && (r < y) For ...
user avatar
1 vote
0 answers
60 views

How to convert wp equations into linear algebra equations?

I am reading this paper [1], wherein the authors first formulated a safety constraint in terms of wp equations. Then, they converted the equations into linear algebra form. As per section 4.3, their ...
desert_ranger's user avatar
1 vote
0 answers
144 views

How to deal with missing variables when utilizing weakest precondition for verification?

I am reading the example given in [1], section 4.2. It deals with applying weakest precondition (wp) rules to ensure that the velocity of a car doesn't exceed a certain limit. We have the following ...
desert_ranger's user avatar