# Questions tagged [hoare-logic]

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

73 questions
Filter by
Sorted by
Tagged with
16 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} ...
13 views

### Companion volume to Concurrency verification of Willem-Paul de Roever

At the moment I am working hard with the book "Concurrency Verification Introduction to Compositional and Non-compositional Methods" written by Willem-Paul de Roever et al. In the ...
28 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 ...
27 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 ...
23 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 ...
105 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 ...
44 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: ...
16 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 ...
138 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 ...
335 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 ...
34 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 ...
104 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 ...
97 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 := ...
26 views

54 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: ...
241 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 ...
247 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 ...