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
3 votes
0 answers

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 ...
Zooky's user avatar
  • 131
3 votes
0 answers

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, ...
reinierpost's user avatar
  • 5,359
2 votes
0 answers

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 ...
BoiD's user avatar
  • 21
2 votes
0 answers

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, ...
Mad A.'s user avatar
  • 143
1 vote
0 answers

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 ...
Mateusz Piotrowski's user avatar
1 vote
0 answers

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 ...
Joe Rakhimov's user avatar
1 vote
0 answers

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: ...
Data's user avatar
  • 215
1 vote
0 answers

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 ...
Lance's user avatar
  • 2,163
1 vote
0 answers

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 ...
HorribleATMath's user avatar
1 vote
0 answers

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\...
InfZero's user avatar
  • 183
1 vote
0 answers

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: ...
JBenzie's user avatar
  • 11
0 votes
0 answers

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(...
Salma muhammad's user avatar
0 votes
0 answers

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 ...
Reggie Hurley's user avatar
0 votes
0 answers

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} ...
John Gann's user avatar
  • 101
0 votes
0 answers

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: ...
Bruce's user avatar
  • 1
0 votes
1 answer

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.
40er's user avatar
  • 3
0 votes
0 answers

Hoare Triple Logic

I'm having trouble understanding the logic behind Hoare Triples. The question asks for the missing value of the precondition {X} ...
Redone123's user avatar
0 votes
0 answers

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 ...
August Jelemson's user avatar
0 votes
0 answers

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 ...
Paweł's user avatar
  • 9
0 votes
0 answers

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-...
user60542's user avatar
-1 votes
1 answer

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 ...
user60587's user avatar
-2 votes
1 answer

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 )
Anonymous's user avatar