51
votes
Example of an algorithm that lacks a proof of correctness
Here is an algorithm for the identity function:
Input: $n$
Check if the $n$th binary string encodes a proof of $0 > 1$ in ZFC, and if so, output $n+1$
Otherwise, output $n$
Most people suspect ...
- 274k
19
votes
Accepted
Difference between Dependent type , refinement type and Hoare Logic
There is recent work by Paul-André Melliès and Noam Zeilberger that explores this. In particular the papers Functors are Type Refinement Systems and An Isbell Duality Theorem for Type Refinement ...
- 11.9k
10
votes
Accepted
What was the major breakthrough between Hoare-Floyd logic and Scott–Strachey semantics?
I don't know why people didn't develop Hoare logics for lambda-calculi earlier. The first work to get this right was Honda et al's
A Compositional Program Logic for Polymorphic Higher-Order Functions
...
- 8,268
10
votes
Example of an algorithm that lacks a proof of correctness
Most algorithms have not been proven correct in Hoare logic. The main reason is that such correctness proofs are extremely expensive as of Jan 2017, probably by several orders of magnitude in ...
- 8,268
9
votes
What is a predicate transformer?
The predicate transformer is just a formalization of the idea that you can produce a precondition given a program and its postcondition.
For example, given a program ...
- 209
8
votes
Accepted
Relation between Hoare Type Theory and pointers
A pointer to a variable creates an alias. When the alias is modified, the corresponding variable is modified as well. Therefore, the rule for an assignment in Hoare's logic is not just update the ...
8
votes
Accepted
What does it mean to "strengthen the precondition and weaken the postcondition" in Hoare logic?
Condition $A$ is stronger than condition $B$ if $A$ implies $B$. That is, if $B$ holds in all situations in which $A$ holds. Conversely, if $A$ is stronger than $B$, ...
- 81.1k
6
votes
Intuitive explanation of Hoare assignment axiom
Hoare Logic proceeds backwards. It is a method to compute a precondition such that the desired postcondition holds. In fact, the inference rules given in your standard Hoare Logic deductions compute ...
- 1,057
5
votes
Example of an algorithm that lacks a proof of correctness
Problem: Print "Yes" if every even number ≥ 4 is the sum of two primes, and "No" if there is an even number ≥ 4 that is not the sum of two primes.
Algorithm: Print "Yes"
Most people think that the ...
- 27.4k
5
votes
Example of an algorithm that lacks a proof of correctness
This is tied to the incompleteness of the underlying logic. Indeed, Hoare logic usually contains a weakening or "pre-post" rule
$$
\dfrac{
P \implies P'
\qquad
\{P'\}c\{Q'\}
\qquad
Q' \implies Q'
}{
\{...
- 14.4k
5
votes
Accepted
Find the loop invariant of the given while loop
At the end of each iteration you have
$$
\forall j: 0 \leq j < i \implies b[j] = a[j+1]
$$
which you can prove by induction. Thus, when the algorithm terminates, $i$ has reached $n-1$ and you have ...
- 1,048
4
votes
Accepted
Proving the loop invariant for a simple program in Hoare logic
Your invariant, together with the negation of the loop condition, is not strong enough to imply your postcondition. Try adding an additional conjunct to the invariant which, together with $\neg\ i<...
- 2,158
4
votes
Accepted
Hoare logic - total correctness of loops
They are equivalent, in the sense that every time you can apply the textbook rule you can also apply your own rule, and vice versa. The invariant for the two rules is similar, but not the same.
...
- 14.4k
4
votes
Finding weakest precondition
Weakest precondition (WPC) can be computed with a procedure that takes your program, as well as the given postcondition (in this case, x=y), as inputs, and applies ...
- 540
4
votes
Accepted
what is the 'x :=' part mean in a hoare triple?
Short answer, it's an assignment, but it's not part of Hoare logic.
It means whatever it means in the programming language you're using.
A Hoare triple in general looks like $\{P\}\; C\; \{Q\}$ (...
- 17.9k
4
votes
Accepted
The difference between a Hoare Triple/Assertion and a Typed Function
You are putting your finger on angular stone of program verification.
At a very rough and high level you can think a derivation in Hoare logic as proving a property, thing which can somehow be ...
- 364
4
votes
Accepted
Hoare logic, proving conjunction rule from basic rules, possible or not?
Your reasoning is fine as far as the derivability of this rule. To respond to the latter part of your last paragraph, if the rules you've listed are all the rules available, then those are the only ...
- 11.9k
3
votes
Accepted
Continuation-passing style: what is meant by "CPS'ing"?
I had only a quick look at the paper, but I believe that they are referring to moving from
$$
t_1 \to t_2 \cdots \to t_n
$$
to
$$
t_1 \to t_2 \cdots \to \lnot \lnot t_n
$$
where $\lnot t = (t \...
- 14.4k
3
votes
Accepted
How to prove the equivalence between Hoare and Floyd assignment axioms?
but when I try $F = G[v/e]$ then from $\exists v' (F[v/v'] \land v=e[v/v'])$ I can't obtain $G$.
We can assume $v'$ not free in $G$. Then, we have
$$
\begin{array}{ll}
& \exists v' (F[v/v'] \...
- 14.4k
3
votes
Accepted
Check whether loop invariants are correct?
Rather than telling you whether your specific invariants are correct, let me teach you the procedure for how you can check whether your invariants are correct on your own.
Basically, you break it ...
D.W.♦
- 152k
3
votes
Accepted
Why precondition strengtening is sound in Hoare logic
The triple $\{Q\}C\{X\}$ states that if $Q$ holds, then after executing $C$, the condition $X$ holds. Now suppose that $\{Q\}C\{X\}$ and that $P \Longrightarrow Q$. We will prove that $\{P\}C\{X\}$. ...
- 274k
3
votes
Example of an algorithm that lacks a proof of correctness
Any algorithm that is correct but we don't know how long it takes to run can be transformed into an algorithm that stops in a guaranteed amount of time but we aren't sure if it is correct.
For ...
- 169
3
votes
Accepted
Developing invariants for comparing two strings
I would not simplify $(2)$ at all. Just apply the rules for if, =, and command composition. Use weakening (pre- or post- rules) ...
- 14.4k
3
votes
Accepted
Hoare-Logic: Requirements for imperfect data types
No, when using Hoare logic properly, you make sure to account for integer overflow etc. and model the full semantics of the programming language.
It is possible to use Hoare logic along the lines you ...
D.W.♦
- 152k
3
votes
Accepted
Understanding Hoare Logic Axioms
Here are some answers and hints to pursue your reflexions.
$\mathtt{Assignment}$
What $\phi([x \leftarrow E])$ means. You said yourself that the semantic of the precondition confuses you that was ...
- 364
3
votes
The difference between a Hoare Triple/Assertion and a Typed Function
To be frank, it much more difficult to see how types and pre-/post-conditions are similar than how they differ.
In Hoare Logic, for the Hoare triple $\{A\}\ f\ \{B\}$, $A$ and $B$ would be predicates ...
- 11.9k
3
votes
Accepted
How to prove a side effect in a function
If the function has two outputs, a standard way to represent this is as a function $f: A \to (B \times C)$, i.e., $f$ outputs a pair of an AST and a symbol table.
If the function updates an existing ...
D.W.♦
- 152k
3
votes
How to prove a side effect in a function
It depends on how you model the system and what proof approach you're using. For early versions of Hoare Logic, there isn't really any notion of "scope", so there's absolutely nothing special you need ...
- 11.9k
3
votes
Accepted
The Law of Excluded Miracle in the language of guarded commands
The answer I can provide is I was reusing the definition of weakest precondition from the IMP language, but in fact I need a stronger definition. This definition looks as follows:
...
- 2,230
3
votes
Accepted
I cannot find an invariant for the following program
Figure out what the value of y is, depending on x, a, and c. Prove that your formula is correct before the first iteration, and prove that if it is true before an iteration then it is also true after ...
- 27.4k
Only top scored, non community-wiki answers of a minimum length are eligible