Questions tagged [hoare-logic]

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

Filter by
Sorted by
Tagged with
0
votes
1answer
65 views

Hoare triple: Loop invariant and correctness

The following Hoare triple in which variable a is an array of integers, and len, max, i, n, j and m are integer-valued variables. Provide a loop invariant (using predicate logic) suitable for proving ...
0
votes
1answer
53 views

Confusion about assignment axiom in Hoare logic

I wanted to know if we are given the f.f.g. Hoare triple: {x = 43}x := x + 1{x = 44} How do we show that this is a valid Hoare triple? My attempt was: Using the assignment axiom: {x + 1 = 43} x := ...
7
votes
1answer
210 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 ...
0
votes
0answers
28 views

Using Hoare logic to show an invariant holds or using induction?

I want to know if given a while loop: x = 0 while(x < 5){ x = x + 1 } I want to show that x (at the a ith iteration of the loop), the value of i is ...
0
votes
0answers
18 views

How to solve Hoare's problem when precondition contains meta symbols?

This is the proram for which I have to prove correctness using Hoare's Axioms: {X = |x|} if(x<=0) x:=-x; else skip; {X=x} This is my solution so ...
3
votes
1answer
130 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 ...
2
votes
0answers
21 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))=\...
2
votes
0answers
65 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 ...
1
vote
0answers
43 views

Can we ignore the postcondition in the Hoare conditional rule when there is a return statement?

I'm proving the correctness of naive string matching using Hoare logic. I have the following pseudocode: ...
2
votes
1answer
84 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 ...
2
votes
1answer
37 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 ...
0
votes
1answer
40 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 = ...
0
votes
2answers
60 views

Using the Consequence Rule

I have the following example that I have to prove {a>7 ^ b>=0} n:=a-b {n<a ^ a+b>=0} Using the Consequence Rule I assumed that the P is true ...
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 ...
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
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 ...
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\\ &\}\\...
2
votes
1answer
139 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\...
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
21 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 ...
1
vote
1answer
82 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 ...
2
votes
1answer
126 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. ...
0
votes
1answer
61 views

Inference rules for deriving invariants in Hoare logic

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
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): ...
0
votes
1answer
2k views

Finding weakest precondition

I have the following program x := y + 1; if (y > 0) then x := x + y else x := y + 100; x := x + y; I want to compute the weakest precondition for getting <...
1
vote
2answers
798 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-...
1
vote
1answer
61 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?
0
votes
0answers
127 views

Counting the number of occurences - loop invariant

I'm trying to come up with loop invariant for the following program. k = a[0] m = 1 p = 1 while p < n: if a[p] == k: m += 1 p += 1 return m I ...
1
vote
1answer
137 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 ...
1
vote
1answer
356 views

How to get Loop invariants to prove program is correct in Hoare logic

start off stating the definition of a loop invariant. It is a condition that must be true at the start of the loop and must be true after each iteration of the loop. I understand what it is but i have ...
3
votes
0answers
254 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 ...
4
votes
1answer
107 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 continuation-...
1
vote
0answers
63 views

Hoare correctness proof for a recursive definition of multiplication

Given the program: {y=y0 ^ y>=0} z=0; while (y>0){ z=z+x; (1) y=y-1; } {z=x*y0} I am having trouble finding the ...
1
vote
1answer
100 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 ...
5
votes
1answer
117 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 ...
0
votes
1answer
136 views

Why does (y < 10) imply everywhere (x > 0 ^ y < 10)?

My lecturer recently released solutions to an assignment. One of the questions was to determine the weakest precondition of: ...
7
votes
1answer
282 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 ...
2
votes
1answer
798 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: ...
18
votes
5answers
5k 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 ...
4
votes
2answers
2k 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 ...
11
votes
2answers
1k 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 ...
5
votes
3answers
550 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 \...
3
votes
1answer
43 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 ...
-1
votes
1answer
41 views

Does this program satisfy the postcondition?

Does the following program $P$: a = 2 b = a + 3 c = a * b Satisfy the following formula? $$\{ \top \} \; P \; \{ a < (b - 2) + c \}$$ I want to use integers ...
0
votes
0answers
337 views

How can I find the strongest postcondition for those two Hoare triples?

I'm trying to solve an exercise in which I have to find the strongest post-condition of the two Hoare triples. \begin{gather*} (| a=9 |)\ a=2; b=a+1; a=b*b;\ (| ?? |)\\ (| i=-j |)\ i=i+1; j=j-...
1
vote
0answers
23 views

How to define the dimension function for searching in a 3D-array?

Problem: Propose a plan (pre- and post-condition, invariant, dimension function) for searching a value in a 3D-array. Solution: This is the first solution I've foreseen: $[\text{Ctx}\ C: m\...
2
votes
2answers
70 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}...
3
votes
1answer
778 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 ...
2
votes
1answer
295 views

Hoare logic - invariant of loop [closed]

I am trying to prove partial corectness of following program: ...
1
vote
0answers
222 views

I need help understanding how to prove partial correctness

Please help me understand how I would prove the partial correctness of the below pseudocode with respect to the following predicates: Pre: {n>=0} Post: ...