Podcast #128: We chat with Kent C Dodds about why he loves React and discuss what life was like in the dark days before Git. Listen now.

# Questions tagged [hoare-logic]

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

65 questions
Filter by
Sorted by
Tagged with
463 views

### Hoare logic - partial/total correctnes and strength invariant

I'm studying Hoare logic and I can't understand the relation between partial and total correctness regarding loop invariant. Suppose for example that I have the following program: ...
67 views

### Does this loop invariant guarantee that the variable never changes?

Suppose you have some loop and and integer k: int k = 5; for (int i = 0 ; i < N; i++) { //(*) //do something } The loop invariant at (*) is: $\{ K=k\}$ ...
70 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 := ...
61 views

### Inference rules for deriving invariants in Hoare logic

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
3k views

### Finding weakest precondition

I have the following program x := y + 1; if (y > 0) then x := x + y else x := y + 100; x := x + y; I want to compute the weakest precondition for getting <...
61 views

### Using the Consequence Rule

I have the following example that I have to prove {a>7 ^ b>=0} n:=a-b {n<a ^ a+b>=0} Using the Consequence Rule I assumed that the P is true ...