# Tag Info

50

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 this algorithm computes the identity function, but we don't know, and we can't prove it in the commonly accepted framework for mathematics, ZFC.

18

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 Systems. There's also a video of a talk on the first one. I think there is a lot of confusion around refinement types due to people thinking of particular systems ...

10

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 comparison with 'mere' programming. There is a lot of ongoing work to reduce this cost by automation, but it's an uphill struggle. Another reason why an algorithm ...

10

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 There were some earlier attempts before this, but they didn't quite nail the problem, for example: how do you denote the value of a functional program? What ...

8

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 value, but update the value for all associated aliases. Let's apply it to the example: {True} int i=0; {i = 0} {i = 0} int*p=&i; {i = 0; [*p, i]} ...

8

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$, then $B$ is weaker than $A$. Note that, from the definition, $A$ is stronger and weaker than itself, since $A$ implies $A$. (We might prefer to ...

7

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 sqrt with the postcondition that sqrt(x) = y and y*y = x, what are some valid preconditions? x > 10 x > 20 x > 1 Some invalid preconditions would be x < 0 x > -10 One predicate P1 is ...

6

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 weakest preconditions, or the most "specific" precondition that still guarantees that the post-condition holds at the next program point. I think this is the ...

5

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' }{ \{P\}c\{Q\} }$$ where the implications $P\implies P', Q\implies Q'$ need to be proved in an underlying logic, usually First-Order Logic (FOL) with some set-...

5

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 algorithm is correct. There is no known proof, and it is quite possible that there is no proof.

5

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 $$\forall j: 0 \leq j < n-1 \implies b[j] = a[j+1]\,.$$ I figured this out by just asking myself what kind of statement I can make at the end of each ...

4

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. Converting a textbook rule instance into an instance of your rule Suppose we have an application or your textbook rule. I.e., we have found some $\texttt{I}$ for ...

4

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<10$, implies $i=10$ (the $j=-1$ part then follows from $i+j=9$).

4

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\}$ (stolen from the all-knowing wiki), where: $P$ and $Q$ are assertions about the state of the system before and after $C$ is executed; and $C$ is some piece of code....

4

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 translated in a type derivation. More precisely you are almost (you're slightly limiting yourself with Hoare logic) rediscovering the very deep Curry-Howard ...

3

The loop invariant doesn't "guarantee" anything. It is a summary of relevant information you know about the state of the program when it reaches that point. If your loop is e.g.: k = 5; ... for(int i = 0; i < N; i++) { /* Invariant: k = 5 */ ... k = 207; ... frob_very_hard(&k); ... k *= 3; ... k = 5; } at the marked point ...

3

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 example, to find a prime larger than $n$, start counting up from $n+1$ testing if each number is prime until you find one. Now modify it to give up and return $0$ if ...

3

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'] \land v=e[v/v']) \\ \iff & \mbox{\{def. F\}}\\ & \exists v' (G[v/e][v/v'] \land v=e[v/v']) \\ \iff & \mbox{\{property of H[v/-][v/-]\}}\\ & \... 3 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 down by looking at each chunk of code separately. For each chunk of code, you look at the invariant before it and after it and see whether they're consistent with ... 3 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\}. Indeed, suppose that P holds. Since P \Longrightarrow Q, also Q holds. Hence if we execute C, then X will hold. Altogether, we see that \{P\}C\{X\} ... 3 Note that the loop is not the outermost construct in your program; that is a sequential composition. In order to apply this rule, you first need to take care of the initial assignments. In this case that is straightforward: you get that the formula x>0\wedge y>0\wedge z=0\wedge u=x holds after z:=0; \ u:=x. For the loop rule, you need three ... 3 You're misunderstanding. It's not that when you try to prove total correctness, Hoare logic somehow magically finds a stronger invariant for you. Hoare logic doesn't find the invariant for you -- either way, you have to find the invariant yourself and then prove it. Rather, it's that you need to prove a stronger invariant if you want to prove total ... 3 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 \to r) for some fixed return type r. In the paper, they choose r = \sf Type. So, we get$$ t_1 \to t_2 \cdots \to (t_n \to {\sf Type}) \to {\sf Type} $$... 3 I would not simplify (2) at all. Just apply the rules for if, =, and command composition. Use weakening (pre- or post- rules) when convenient to do so. Below, I added an empty else branch for clarity. // (2): (S1 = S2 <=> X = Y \land E = true) // \land \lnot(X != /\ \land Y != /\ \land E = true) if !(X == /\ and Y == /\) // (3a): (2) \... 3 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 suggest, but the problem with that is that it invalidates all guarantees you might have hoped for. Since the whole point of Hoare logic is to obtain ... 3 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 what the assignment x := E was doing. But in fact your are precisely pointing out the crux of this rule: it affects the precondition exactly as the assignment ... 3 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 on the entire program state and f would be a sequence of instructions, not a function. For example, A might be something like$$\mathtt i = 0\land \mathtt ...

3

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 symbol table, you could represent this as a function $f : (A \times C) \to (B \times C)$. It takes as an input a pair of a string and a symbol table, and ...

3

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 to do. You simply have a pre-conditions and post-conditions on the global state. For Hoare Logic, types have nothing to do with it. In a bit more detail, in a ...

3

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: definition "wp c Q s ≡ (∃t. (c,s) ⇒ t) ∧ (∀ t'. (c,s) ⇒ t' ⟶ Q t')" It is taking care of non-determinism. When one evaluates: lemma excluded_miracle: "wp c (λ t. False) = (λ s. ...

Only top voted, non community-wiki answers of a minimum length are eligible