# Questions tagged [hoare-logic]

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

17 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
285 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 ...
93 views

### Spot the formalism (some kind of process logic)

Consider the following specification technique. A specification consists of a finite set of triples $\langle C, A, C' \rangle$, where $A$ is the name of an action and $C, C'$ are conditions, that is, ...
22 views

233 views

### I need help understanding how to prove partial correctness

Please help me understand how I would prove the partial correctness of the below pseudocode with respect to the following predicates: Pre: {n>=0} Post: ...
12 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. ...
32 views

### Using Hoare logic to show an invariant holds or using induction?

I want to know if given a while loop: x = 0 while(x < 5){ x = x + 1 } I want to show that x (at the a ith iteration of the loop), the value of i is ...
20 views

### How to solve Hoare's problem when precondition contains meta symbols?

This is the proram for which I have to prove correctness using Hoare's Axioms: {X = |x|} if(x<=0) x:=-x; else skip; {X=x} This is my solution so ...
139 views

### Counting the number of occurences - loop invariant

I'm trying to come up with loop invariant for the following program. k = a m = 1 p = 1 while p < n: if a[p] == k: m += 1 p += 1 return m I ...
Does the following program $P$: a = 2 b = a + 3 c = a * b Satisfy the following formula? $$\{ \top \} \; P \; \{ a < (b - 2) + c \}$$ I want to use integers ...