Questions tagged [hoare-logic]
Questions about Hoare's logical framework for program correctness proofs and variants.
79
questions
0
votes
1
answer
146
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:
...
- 11
7
votes
1
answer
367
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 ...
- 73
8
votes
1
answer
304
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 ...
- 2,184
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:
...
- 234
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 ...
- 952
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 \...
- 1,055
3
votes
1
answer
75
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 ...
- 43
5
votes
2
answers
5k
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 ...
- 495
-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 ...
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
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
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}...
- 183
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 ...
- 183
2
votes
1
answer
385
views
Hoare logic - invariant of loop [closed]
I am trying to prove partial corectness of following program:
...
user54001
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
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 ...
- 933
4
votes
1
answer
1k
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
...
- 421
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:
...
- 317
3
votes
1
answer
402
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 ...
- 162
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
0
votes
1
answer
1k
views
Finding a Hoare logic correctness proof for a Repeat-Until loop
How can we prove a program in repeat until using Hoare Logic?
I've found a rule like this:
{P} S {R}, {R ^ ~B -> P}, {R ^ B -> Q}
for
...
0
votes
1
answer
579
views
Hoare logic - partial/total correctnes and strength invariant
I'm studying Hoare logic and I can't understand the relation between partial and total correctness regarding loop invariant. Suppose for example that I have the following program:
...
- 155
0
votes
2
answers
539
views
Hoare Calculus Incorrect Assignment Axiom
I'm currently preparing for an exam and recently came across the following exercise and would like to know whether my solution would be correct.
Exercise:
Prove that the following axiom is not ...
- 113
2
votes
1
answer
303
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 ...
- 123
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.] ...
- 621
0
votes
1
answer
96
views
Does this loop invariant guarantee that the variable never changes?
Suppose you have some loop and and integer k:
int k = 5;
for (int i = 0 ; i < N; i++)
{
//(*)
//do something
}
The loop invariant at (*) is:
$\{ K=k\}$
...
- 287
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
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 ...
- 374
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 ...
- 72k