# Tag Info

## Hot answers tagged hoare-logic

### 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 ...
• 278k
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,328

### 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,328

### 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 ...
• 219
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 ...
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$, then $B$ is weaker than $A$. ...

### 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,097

• 14.6k
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.6k

### 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

### Intuitive explanation of Hoare assignment axiom

The precondition is in fact the weakest (liberal) precondition that guarantees a valid Hoare triple for that postcondition and assignment statement. ("liberal" because termination is not considered.) ...
• 917
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 ...
• 162k
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

### 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 ...
• 12.1k
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 ...
• 162k

### 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 ...
• 12.1k
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,194
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 ...
• 31k
Accepted

### Why is the assignment rule the way it is in Hoare Logic?

So after reading and thinking about it more this is my explanation (thanks software foundations): The key confusion for me seems to be the meaning of $P[e/x]$ (replaces every free instance of x with ...
• 3,060
Accepted

### What's the meaning of the $\top$ symbol in a Hoare triple?

The symbol $\top$, known as top, stands for "True". There is also a symbol $\bot$, known as bottom, which stands for "False". Top is always true, and bottom is always false. In your case, having a ...
• 278k

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