Questions tagged [hoare-logic]

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

22 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
5
votes
1answer
87 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 ...
3
votes
0answers
382 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 ...
3
votes
0answers
94 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, ...
2
votes
0answers
23 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
95 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 ...
2
votes
0answers
171 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, ...
1
vote
0answers
14 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
0answers
98 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 ...
1
vote
0answers
53 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: ...
1
vote
0answers
81 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
0answers
80 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
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\...
1
vote
0answers
259 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: ...
0
votes
0answers
23 views

How to determinne the loop invariant?

The following code returns the number of trailing zeros of an integer x (number of 0s at the end of the decimal number representation of x). I had to find its loop invariant, which is ...
0
votes
0answers
13 views

Verification conditions for Hoare

I am reading about Hoare logic but I don't really understand the verification conditions part for proving partial correctness. What's happening between step 1 to 2? Why do we ignore the Q := 0 and ...
0
votes
0answers
14 views

Finding bound function of loop invariant

In Programming in the 1990s, by Edward Cohen, the author gives an example of a bound function. For example, if we have $B \equiv 10 - n$ where $n = 0$, say, then $B$ will eventually be falsified if ...
0
votes
0answers
28 views

Textbook for Hoare logic

I am looking to understand what Hoare logic is, and how it is used to prove program-correctness. I am interested in an applied text, which shows how to actually state formal specifications of programs,...
0
votes
0answers
16 views

Proving a Hoare Triple does not hold

I have this program specification annotated with a Hoare Triple. Trying to prove that is the case. ...
0
votes
0answers
34 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
194 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 ...
0
votes
0answers
411 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
1answer
44 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 ...