Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [hoare-logic]

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

25 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
3 votes
0 answers
801 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 ...
Zooky's user avatar
  • 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, ...
reinierpost's user avatar
  • 5,694
2 votes
0 answers
175 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 ...
BoiD's user avatar
  • 21
2 votes
0 answers
246 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, ...
Mad A.'s user avatar
  • 143
1 vote
0 answers
60 views

How to convert wp equations into linear algebra equations?

I am reading this paper [1], wherein the authors first formulated a safety constraint in terms of wp equations. Then, they converted the equations into linear algebra form. As per section 4.3, their ...
desert_ranger's user avatar
1 vote
0 answers
144 views

How to deal with missing variables when utilizing weakest precondition for verification?

I am reading the example given in [1], section 4.2. It deals with applying weakest precondition (wp) rules to ensure that the velocity of a car doesn't exceed a certain limit. We have the following ...
desert_ranger's user avatar
1 vote
1 answer
134 views

Hoare Logic: Identifying Hoare Triple given a simple function

The program is designed to start with values for $x$ and $y$. The variables $u1$​ and $u2$​ are intended to represent $x$ and $y$ in ascending order. Provide suitable preconditions and postconditions ...
User's user avatar
  • 9
1 vote
0 answers
29 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 ...
Mateusz Piotrowski's user avatar
1 vote
0 answers
114 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 ...
Joe Rakhimov's user avatar
1 vote
0 answers
81 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: ...
Data's user avatar
  • 215
1 vote
0 answers
178 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 ...
Lance's user avatar
  • 2,243
1 vote
0 answers
158 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 ...
HorribleATMath's user avatar
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\...
InfZero's user avatar
  • 183
1 vote
0 answers
312 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: ...
JBenzie's user avatar
  • 11
0 votes
0 answers
20 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(...
Salma muhammad's user avatar
0 votes
0 answers
69 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 ...
Reggie Hurley's user avatar
0 votes
0 answers
17 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} ...
John Gann's user avatar
  • 101
0 votes
0 answers
60 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: ...
Bruce's user avatar
  • 1
0 votes
0 answers
55 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} ...
Redone123's user avatar
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 ...
August Jelemson's user avatar
0 votes
0 answers
464 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 ...
Paweł's user avatar
  • 9
0 votes
0 answers
758 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-...
user60542's user avatar
-1 votes
0 answers
12 views

There is a formal methods(like Hoare logic etc) to find a precondition from given post condition, what are informal methods to find pre-condition

There are formal methods (like Hoare logic etc) to find a precondition from given post condition, what are informal methods to find pre-condition from given post condition. Sources will also help
Muhammad Zulqarnain Malik's user avatar
-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 ...
user60587's user avatar
-2 votes
1 answer
95 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 )
Anonymous's user avatar