# Questions tagged [hoare-logic]

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

72 questions
Filter by
Sorted by
Tagged with
20 views

### Show postcondition i:=i+1 using Hoare assginment rule

as far as I understand the hoare assignment rule works like: {i+1=3}i:=i+1{i=3} E.g. to get the precondition I take the postcondition {i=3} and replace every ...
94 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 ...
33 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: ...
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 ...
17 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 ...
77 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 ...
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,...
285 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 ...
18 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. ...
33 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 ...
99 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 ...