# Questions tagged [hoare-logic]

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

79 questions
Filter by
Sorted by
Tagged with
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.
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 ...
5k views

### What does it mean to "strengthen the precondition and weaken the postcondition" in Hoare logic?

Having learned a rough summary of Hoare logic (i.e. learning just the basic concept of Hoare triples and a few of the rules) I kept seeing a statement along these lines: The rule of consquence ...
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: ...
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, ...
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 )
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
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 ...
41 views

431 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 ...
1 vote
359 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 ...
1 vote
917 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 ...
754 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 ...