Questions tagged [hoare-logic]
Questions about Hoare's logical framework for program correctness proofs and variants.
22
questions with no upvoted or accepted answers
3
votes
0
answers
754
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
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,
...
- 5,359
2
votes
0
answers
161
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
2
votes
0
answers
234
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, ...
- 143
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 ...
1
vote
0
answers
112
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
1
vote
0
answers
73
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
1
vote
0
answers
168
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,163
1
vote
0
answers
148
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
1
vote
0
answers
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\...
- 183
1
vote
0
answers
308
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: ...
- 11
0
votes
0
answers
18
views
Evaluate under Hoare logic
Evaluate
WP(a = i + 2; i=i+1, ((a=6)^(i=5))
WP(x=x+1,y=y-1. (xxy>0))
wp(if x > 2 then y = 1 else y = -1,(x > 0))
wp(while n <> 0 do n:=n-1; n = 10)
wp(while n = 0 do n:=n-1; n=-10)
wp(...
0
votes
0
answers
42
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
51
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
1
answer
61
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
0
votes
0
answers
47
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
0
votes
0
answers
431
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
0
votes
0
answers
726
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
votes
1
answer
51
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 ...
-2
votes
1
answer
76
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 )
