StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>In x ⊢ y, x is a set of assumptions, and y is a statement (in the logical system or language you're talking about). "x ⊢ y" says that, in the logical system, if you start with the assumptions x, you can prove the statement y.</p> <p>Because x is a set, it can also be the empty set. Often this is written with the empty set symbol, as ∅ ⊢ y, but sometimes for brevity it is left out completely, which is what's going on here. Being able to prove it from the empty set of assumptions means that it is just true (or valid). For example, ⊢ p → p.</p> <p>Hoare's paper talks about a language for describing the behaviour of programs. As Todd points out, "P {Q} R" is (in this language) the statement that, if you run program Q in an initial state where P is true, then R will be true afterwards (iff Q terminates). This is the kind of statement you might want to prove using some assumptions. These assumptions would be things at a higher level than the initial state: for example, if you've already proven a simpler but related P' {Q'} R' statement, you might want to assume it to prove the bigger P {Q} R statement.</p> <p>Thus "⊢ P {Q} R" says that the statement "P {Q} R" is true, and you don't need to assume anything.</p> <p>Let's take a stupidly simple example.</p> <p><strong>⊢</strong> x = 3 {y := x} x = 3 ∧ y = 3</p> <p>The statement we're proving is: "If x is 3 at the start, and you run the program y := x, then afterwards x will be 3 and y will be 3." You don't need any assumptions to prove this, it follows from the definition of the language. You could go ahead and use this fact as an assumption to prove something else.</p> <p>x = 3 {y := x} x = 3 ∧ y = 3 <strong>⊢</strong> x = 3 {y := x; z := y} x = 3 ∧ y = 3 ∧ z = 3</p> <p>Here we've used the simpler statement on the left as an assumption to prove a bigger statement. It's a very silly example, but I hope it shows how to read this. I've made the ⊢ bold to show it is the "top-level" thing in the line, separating the assumptions from the conclusion. Both the left-hand and right-hand sides are statements in Hoare's logic, with P {Q} R, where P and R are logical statements and Q is a program.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload