Questions tagged [hoare-logic]
Questions about Hoare's logical framework for program correctness proofs and variants.
79
questions
0
votes
0
answers
29
views
Hoare's partition original method
So I was reading the Hoare's partition part of the Quicksort wiki and it says:
"With respect to this original description, implementations often make minor but important variations. Notably, the ...
0
votes
0
answers
11
views
Why is the strongest postcondition for a program that just allocates x "exists x :: P"
I'm working my way through Leino's "Program Proofs" and I was following as far as the semantics of variable assignment, but I'm not quite sure why this is a valid Hoare triple:
{forall x::Q} ...
- 101
0
votes
0
answers
44
views
Hoare triple: introducing Loop invariant and partial correctness
Hoare Triple formalizes program correctness, which contains postcondition, program and precondition such as $\vdash P \{Q\} R$
Provided code snippet:
...
- 1
0
votes
0
answers
24
views
Hoare Logic - Interpreting identity
I'm having some issues on understanding the following identity:
{ P } S { Q } ≡ [P ⇒ wp.S.Q]
Does this means that if I have something like:
...
- 1
0
votes
1
answer
54
views
Hoare Triple Derivation Example (Precondition False)
How can i derive this Hoare Tripel?
{false} x := x + 1; {x = 0}
I do not know which rule should i use on this.
I am confused on this wrong precondition.
- 3
-2
votes
1
answer
73
views
Use Hoare axiom for array-componenet assignment to determine the weakest pre-condition
ASSERT( P ) /* determine what is P */
A[i] = A[m];
A[k] = 2;
ASSERT( A[i] == x + 5 )
1
vote
1
answer
72
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 ...
- 111
1
vote
1
answer
168
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, ...
- 11
0
votes
0
answers
42
views
Hoare Triple Logic
I'm having trouble understanding the logic behind Hoare Triples. The question asks for the missing value of the precondition {X}
...
0
votes
0
answers
33
views
How to prove a segment of a program (Hoare-logic)
Problem:
A segment of a program is shown below:
⋮
_ _ _ _ _ _
z = x - 7;
(|z = 5 ∧ n = 4|)
⋮
What is the dashed line hiding?
My solution:
I think the dashed line ...
- 113
1
vote
1
answer
79
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 ...
- 113
5
votes
2
answers
182
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 ...
- 51
1
vote
1
answer
137
views
Hoare Logic for Factorial
I came across this hoare logic for factorials but I don't quite understand it. We multiply F and X but we're not adding up all values of F so how do we get the sum/factorial at the end?
Precondition: ...
- 167
1
vote
0
answers
27
views
Is true * true = true in Separation Logic?
I am trying to show that the following interference is unsound in terms of Separation Logic:
$$
(p_0 \implies p_1) \implies ((p_0 * q) \implies (p_1 * q))
$$
I came up with the following values for ...
0
votes
1
answer
969
views
How to find the loop invariant in hoare triples
Hey I am new to Hoare triples, and I can't understand on finding the loop invariants in hypothesis. For example this while loop
...
- 103
4
votes
2
answers
593
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 ...
- 2,960
0
votes
1
answer
50
views
I cannot find an invariant for the following program
I have the following:
(|$y=0; x=c$|) while(x > 0){y=y+a; x=x-1;} (|$y= a*c$|)
This seems like a fairly simple program and I can intuitively tell that the post ...
- 157
1
vote
0
answers
111
views
How to prove program solves the problem?
I am preparing for the exam on Theory of Programming class. Now I am trying to solve the task from the sample paper:
Task description starts here
Given the following problem:
A problem is given by ...
- 69
0
votes
1
answer
176
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 := ...
- 261
3
votes
1
answer
41
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))=\...
- 233
0
votes
1
answer
224
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 ...
- 21
2
votes
0
answers
144
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 ...
- 21
1
vote
0
answers
69
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:
...
- 215
3
votes
1
answer
486
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 ...
- 189
3
votes
1
answer
471
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,240
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 ...
- 23
0
votes
1
answer
97
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 = ...
- 13
1
vote
2
answers
103
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,153
1
vote
1
answer
174
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,153
4
votes
2
answers
176
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,153
1
vote
1
answer
257
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,153
2
votes
1
answer
300
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,153
1
vote
0
answers
162
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,153
1
vote
1
answer
42
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 ...
- 659
1
vote
1
answer
199
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 ...
user87320
2
votes
1
answer
327
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.
...
- 123
0
votes
1
answer
82
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):
...
- 9,461
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,461
1
vote
1
answer
77
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?
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-...
0
votes
0
answers
426
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 ...
- 9
1
vote
1
answer
351
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 ...
- 45
0
votes
1
answer
6k
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 <...
- 101
1
vote
1
answer
872
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 ...
- 13
4
votes
1
answer
202
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 ...
- 357
3
votes
0
answers
717
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 ...
- 131
1
vote
0
answers
139
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 ...
- 111
0
votes
2
answers
213
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
1
answer
225
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 ...
- 13
5
votes
1
answer
223
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 ...
- 53