# Questions tagged [hoare-logic]

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

79 questions
Filter by
Sorted by
Tagged with
18 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(...
42 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 ...
11 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} ...
51 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: ...
61 views

### 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.
76 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 )
1 vote
78 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 ...
1 vote
188 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, ...
47 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} ...
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 ...
1 vote
111 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 ...
189 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 ...
1 vote
152 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: ...
1 vote
27 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 ...
1k 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 ...
666 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 ...
57 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 ...
1 vote
112 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 ...
181 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 := ...