# Questions tagged [hoare-logic]

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

69 questions
Filter by
Sorted by
Tagged with
6k views

### Example of an algorithm that lacks a proof of correctness

We have Hoare logic. Why is it still possible that an algorithm is right but there is no proof that it's correct? Suppose the algorithm is expressed in C. Then we can argue step by step that it's ...
2k views

### Difference between Dependent type , refinement type and Hoare Logic

I know little dependent type theory. From wikipedia : A dependent type is a type whose definition depends on a value. And from my Type theory course i recall that a dependent type is : Family ...
1k views

### How to deal with arrays during Hoare-style correctness proofs

In the discussion around this question, Gilles mentions correctly that any correctness proof of an algorithm that uses arrays has to prove that there are no out-of-bounds array accesses; depending on ...
222 views

### What was the major breakthrough between Hoare-Floyd logic and Scott–Strachey semantics?

I'm reading through a commentary on Milner's "The use of machines to assist in rigorous proof" by Mike Gordon. In this paper, he explains how LCF was born from the ideas of denotational semantics by ...
309 views

### Hoare logic - total correctness of loops

Consider a while loop of the form : $\texttt{while (C) {S}}$ with $\texttt{C}$ the condition and $\texttt{S}$ the body of the loop. Let $\texttt{I}$ and $\texttt{V}$ respectively be an invariant ...
960 views

### Hoare triple for assignment P{x/E} x:=E {P}

I am trying to understand Hoare logic presented at Wikipedia, Hoare logic at Wikipedia Apparently, if I understand correctly, a Hoare triple $$\{P\}~ C ~\{Q\}$$ means if P just before C, then Q ...
626 views

21 views

### Hoare-Logic: Requirements for imperfect data types

Theoretically, Hoare-Logic let's one prove the correctness of an algorithm, given pre- and post-condition. However, as far as I've seen it so far, one idealizes his data-types to a mathematical set ...
113 views

### How to prove the equivalence between Hoare and Floyd assignment axioms?

How to show that these two axioms are equivalent: 1: $\{G[v/e]\} v:=e \{G\}$ 2: $\{F\} v:=e \{\exists v' (F[v/v'] \land v=e[v/v'])\}$ I've tried with $G = \exists v' (F[v/v'] \land v=e[v/v'])$and ...
932 views

### Check whether loop invariants are correct?

I'm trying to prove some code is correct, using Hoare logic. How do I check whether my loop invariants are correct? I'm asked to prove (using Hoare Logic) that the following program is valid: ...
947 views

### how to solve Hoare logic problems

I'm having trouble proving Hoare logic questions as I'm not sure of the process that is taken to prove them. I understand that they're rules such as assignment axiom, pre-condition strengthening, post-...
178 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 ...
41 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 ...
89 views

### How to prove $c = a + b$ using Program Verification Techniques

I am trying to prove an elementary thing, but it seems at some point you get down to atoms where you can't prove anything else. This is why I am wondering about proving $c = a + b$, it seems like an ...
174 views

### How to use Hoare Logic to Prove this Assertion

Given this assertion in Hoare Logic: \begin{align} &\mathbf{\{p >= 0\}}\\ &s = 0 ; n = 1 ;\\ &\mathtt{while}\ (n <= p)\ \{\\ &\quad s = s + n ;\\ &\quad n = n + 1\\ &\}\\...
114 views

### Loop termination - Loop invariant

(x >= 0 && y >= 0) q = 0; r = x; while ( r >=y ) { r = r - y; q = q + 1; } (x = q*y +r) && (r >= 0) && (r < y) For ...
97 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 ...
46 views

### Can we ignore the postcondition in the Hoare conditional rule when there is a return statement?

I'm proving the correctness of naive string matching using Hoare logic. I have the following pseudocode: ...
76 views

### How to apply Hoare Logic to this function

I would like to apply Hoare Logic to realistic, complex imperative programs that use while loops, if statements, functions, modules, etc. and have side effects (e.g. access the network). In order to ...
498 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 ...
76 views

### Hoare correctness proof for a recursive definition of multiplication

Given the program: {y=y0 ^ y>=0} z=0; while (y>0){ z=z+x; (1) y=y-1; } {z=x*y0} I am having trouble finding the ...