# Questions tagged [hoare-logic]

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

82 questions
Filter by
Sorted by
Tagged with
1 vote
136 views

### Hoare Logic: Identifying Hoare Triple given a simple function

The program is designed to start with values for $x$ and $y$. The variables $u1$​ and $u2$​ are intended to represent $x$ and $y$ in ascending order. Provide suitable preconditions and postconditions ...
176 views

### How did this work apply weakest precondition rule on their example car problem?

While reading the example given in [1]., I couldn't understand how the authors set up the logic to compute the weakest preconditions (wp) in their car example in section 4.2. The dynamics of the ...
1 vote
60 views

### How to convert wp equations into linear algebra equations?

I am reading this paper [1], wherein the authors first formulated a safety constraint in terms of wp equations. Then, they converted the equations into linear algebra form. As per section 4.3, their ...
117 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.
1 vote
144 views

### How to deal with missing variables when utilizing weakest precondition for verification?

I am reading the example given in [1], section 4.2. It deals with applying weakest precondition (wp) rules to ensure that the velocity of a car doesn't exceed a certain limit. We have the following ...
20 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(...
74 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 ...
6k 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 ...
60 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
268 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, ...
97 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 )
219 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
95 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 ...
43 views

466 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