The Hoare Cube

https://johnwickerson.wordpress.com/2024/12/04/the-hoare-cube/

by matt_d • 2 years ago

86 16 2 years ago

johnwickerson.wordpress.com

MeetingsBrowser• 2 years ago

I'm just glad to know I'm not the only one who finds some of Cousot's writing to be overwhelming.

mhb• 2 years ago

As will I be to know that about writings about his writing.

PaulHoule• 2 years ago

I've learned the hard way that logic is one of the most depressing subjects.

(Exhibit 1: No single completely satisfactory form of logical negation)

thechao• 2 years ago

My advisor used to go drinking with the Cousots'. He said Cousot becomes more scrutable with more wine. I asked my advisor if he meant Cousots' papers or Cousots' conversation; his answer was "more French".

BtM909• 2 years ago

Can someone ELI5 this, please?

ivanbakel• 2 years ago

The traditional Hoare logic is the "partial correctness" form - if the program state satisfies a precondition, and executing the program terminates with some other state, then the second state satisfies the postcondition. This is "correctness" in the sense it overapproximates all executions: if the postcondition says something about the state being "good", the precondition ensures you end in a "good" state, but perhaps there are more "good" states than actually reachable ones. It's partial because nothing is said about non-terminating executions.

A more recent idea was to flip this correctness logic to get an incorrectness logic, which says if you can reach a "bad" state (this is useful for bug detection.) In such a logic, you only want to know about reachable states, so the formula gets flipped: if the final program state satisfies the postcondition, then there must be a program state satisfying the precondition that can execute the program and terminate in that final state.

The difference between these two logics is one axis of this cube. There are other possible logics: you can ask if a precondition is necessary - that is, is the postcondition only reachable from states satisfying the precondition? It turns out there are two orthogonal approaches to stating such a property, and they form the other two axes of the cube.

waste_monk• 2 years ago

I would never make a moral judgement on a cube.

The Hoare Cube

Related Stories