2022 Developer Survey is open! Take survey.

Questions tagged [hoare-logic]

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

Filter by
Sorted by
Tagged with
-1 votes
1 answer
23 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 )
user avatar
0 votes
1 answer
41 views

Logic foundation for formal verification

What types of logic should one study as foundation before diving into the area of software verification? What I can think of are: Hoare Logic (for proving correctness of imperative programs) Linear ...
user avatar
  • 101
0 votes
0 answers
19 views

Looking for a reference for "structured programming for data structures"

In a talk by Tony Hoare, he said something interesting and I'm looking for more reading on the topic minute 57: "Languages don't recognize the different structuring principles that are being ...
user avatar
1 vote
1 answer
57 views

Hoare's Axiom Scheme Precondition

I have a question about determining preconditions for Hoare's Axiom Scheme. For example, if we have P { x=2 } x==1 and we are trying to determine the precondition, ...
user avatar
0 votes
0 answers
30 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} ...
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 ...
user avatar
1 vote
1 answer
35 views

How to determine the pre and post conditions of a program (Hoare-logic)

Problem Below is a program named X: y = 1; while(y < x){ y = 10 * y; } What does this program X do? What are appropriate pre and post conditions? (Assume ...
user avatar
5 votes
2 answers
155 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 ...
user avatar
1 vote
1 answer
84 views

Hoare Logic for Factorial

I came across this hoare logic for factorials but I don't quite understand it. We multiply F and X but we're not adding up all values of F so how do we get the sum/factorial at the end? Precondition: ...
user avatar
  • 167
1 vote
0 answers
22 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 ...
user avatar
0 votes
1 answer
424 views

How to find the loop invariant in hoare triples

Hey I am new to Hoare triples, and I can't understand on finding the loop invariants in hypothesis. For example this while loop ...
user avatar
4 votes
2 answers
425 views

Why is the assignment rule the way it is in Hoare Logic?

Why is the assignment rule the way it is in Hoare Logic/Axiomatic Semantics? I can't wrap my head around why the assignment rule is backwards from what I expected. I understand Hoare logic is use to ...
user avatar
0 votes
1 answer
37 views

I cannot find an invariant for the following program

I have the following: (|$y=0; x=c$|) while(x > 0){y=y+a; x=x-1;} (|$y= a*c$|) This seems like a fairly simple program and I can intuitively tell that the post ...
user avatar
  • 153
1 vote
0 answers
106 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 ...
user avatar
0 votes
1 answer
121 views

Confusion about assignment axiom in Hoare logic

I wanted to know if we are given the f.f.g. Hoare triple: {x = 43}x := x + 1{x = 44} How do we show that this is a valid Hoare triple? My attempt was: Using the assignment axiom: {x + 1 = 43} x := ...
user avatar
  • 251
3 votes
1 answer
35 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))=\...
user avatar
  • 233
0 votes
1 answer
179 views

Hoare triple: Loop invariant and correctness

The following Hoare triple in which variable a is an array of integers, and len, max, i, n, j and m are integer-valued variables. Provide a loop invariant (using predicate logic) suitable for proving ...
user avatar
  • 21
2 votes
0 answers
118 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 ...
user avatar
  • 21
1 vote
0 answers
58 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: ...
user avatar
  • 215
2 votes
1 answer
360 views

Hoare logic, proving conjunction rule from basic rules, possible or not?

(This is HW.) Suppose I have these following proof rules given. I am currently considering if I can prove the conjunction rule (given below) from the above given Hoare logic rules. My answer would ...
user avatar
  • 179
3 votes
1 answer
343 views

The Law of Excluded Miracle in the language of guarded commands

The definition of weakest precondition is familiar (let me use Isabelle's syntax here): definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t" the weakest precondition ...
user avatar
  • 2,220
2 votes
1 answer
42 views

Bottleneck in Hoare Logic unable to arrive at my {P} from {Q}

{Q} = {n>0} C1 = i := 1; C2 = c := 1; C3 = p := 0; {P} = {i<=n, p = fib(i-1), c = fib(i)} My lack of understanding towards the rule of consequence in hoare logic is blocking me from find the ...
user avatar
0 votes
1 answer
80 views

How to solve for the precondition give a postcondtion that must satisfy two conditions

I tried solving past exam question but there is this one that I haven't been able to solve. The question states that a suitable precondition should be found for the statement. $$ a= i +2; i++\{(a = ...
user avatar
  • 13
1 vote
2 answers
84 views

How to prove a side effect in a function

I asked a question earlier about Saving to the Database, which was very general and about the requirements for a proof when you go through many layers of non-verified systems such as the network and ...
user avatar
  • 1,873
1 vote
1 answer
147 views

How to prove $c = a + b$ using Program Verification Techniques

I am trying to prove an elementary thing, but it seems at some point you get down to atoms where you can't prove anything else. This is why I am wondering about proving $c = a + b$, it seems like an ...
user avatar
  • 1,873
4 votes
2 answers
159 views

The difference between a Hoare Triple/Assertion and a Typed Function

I have been trying to wrap my head around applying Hoare Logic and am running into the question of how Hoare triples are any different from (simply) a typed function. That is, say you have a typed ...
user avatar
  • 1,873
1 vote
1 answer
235 views

How to use Hoare Logic to Prove this Assertion

Given this assertion in Hoare Logic: \begin{align} &\mathbf{\{p >= 0\}}\\ &s = 0 ; n = 1 ;\\ &\mathtt{while}\ (n <= p)\ \{\\ &\quad s = s + n ;\\ &\quad n = n + 1\\ &\}\\...
user avatar
  • 1,873
2 votes
1 answer
245 views

Understanding Hoare Logic Axioms

Given these 5 axioms of Hoare Logic: \begin{array}{cl} \frac{}{\{\phi([x \leftarrow E])\}\ x := E\ \{\phi(x)\}} & \mathtt{Assignment}\\\\ \frac{\{\phi\}\ P_1\ \{\eta\} \quad \{\eta\}\ P_2\ \{\psi\...
user avatar
  • 1,873
1 vote
0 answers
140 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 ...
user avatar
  • 1,873
1 vote
1 answer
34 views

Hoare-Logic: Requirements for imperfect data types

Theoretically, Hoare-Logic let's one prove the correctness of an algorithm, given pre- and post-condition. However, as far as I've seen it so far, one idealizes his data-types to a mathematical set ...
user avatar
  • 629
1 vote
1 answer
182 views

Loop termination - Loop invariant

(x >= 0 && y >= 0) q = 0; r = x; while ( r >=y ) { r = r - y; q = q + 1; } (x = q*y +r) && (r >= 0) && (r < y) For ...
user avatar
2 votes
1 answer
283 views

Find the loop invariant of the given while loop

I don't know how to find a loop invariant. I'm not sure where to start. Can anyone find the loop invariant of the given program and explain your method please. ...
user avatar
0 votes
1 answer
77 views

Inference rules for deriving invariants in Hoare logic

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
user avatar
  • 9,179
4 votes
1 answer
110 views

Developing invariants for comparing two strings

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
user avatar
  • 9,179
1 vote
1 answer
73 views

what is the 'x :=' part mean in a hoare triple?

In Hoare logic, there's a thing called a Hoare triple, e.g.$$ \begin{array}{ccccc} \{x = 2\} & & x := x+1 & & \{x = 3\} \end{array}. $$ What does '$x :=$' mean?
user avatar
1 vote
2 answers
2k views

how to solve Hoare logic problems

I'm having trouble proving Hoare logic questions as I'm not sure of the process that is taken to prove them. I understand that they're rules such as assignment axiom, pre-condition strengthening, post-...
user avatar
0 votes
0 answers
362 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 ...
user avatar
  • 9
1 vote
1 answer
278 views

True Postcondition, with true Precondition

In my exam preparation I stumbled across the follwoing exercise regarding pre and postconditions: As far as I understood the question, we need to express some condition for p, such that if that ...
user avatar
  • 45
0 votes
1 answer
6k views

Finding weakest precondition

I have the following program x := y + 1; if (y > 0) then x := x + y else x := y + 100; x := x + y; I want to compute the weakest precondition for getting <...
user avatar
  • 101
1 vote
1 answer
733 views

How to get Loop invariants to prove program is correct in Hoare logic

start off stating the definition of a loop invariant. It is a condition that must be true at the start of the loop and must be true after each iteration of the loop. I understand what it is but i have ...
user avatar
4 votes
1 answer
175 views

Continuation-passing style: what is meant by "CPS'ing"?

I'm reading Dijkstra Monads for Free for a presentation I'll be doing and it's pretty meaty. One of the things that I keep running into is the term "CPS'ing". I've read a little bit on ...
user avatar
3 votes
0 answers
625 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 ...
user avatar
  • 131
1 vote
0 answers
103 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 ...
user avatar
0 votes
2 answers
166 views

Using the Consequence Rule

I have the following example that I have to prove {a>7 ^ b>=0} n:=a-b {n<a ^ a+b>=0} Using the Consequence Rule I assumed that the P is true ...
user avatar
1 vote
1 answer
200 views

How to prove the equivalence between Hoare and Floyd assignment axioms?

How to show that these two axioms are equivalent: 1: $\{G[v/e]\} v:=e \{G\}$ 2: $\{F\} v:=e \{\exists v' (F[v/v'] \land v=e[v/v'])\}$ I've tried with $G = \exists v' (F[v/v'] \land v=e[v/v']) $and ...
user avatar
5 votes
1 answer
187 views

Relation between Hoare Type Theory and pointers

My understanding is that in Hoare Type Theory every imperative statement has a type of the form {Pre}res:T{Post} where T is the ...
user avatar
0 votes
1 answer
142 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: ...
user avatar
7 votes
1 answer
340 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 ...
user avatar
  • 73
8 votes
1 answer
264 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 ...
user avatar
  • 2,220
2 votes
1 answer
927 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: ...
user avatar
  • 234