On Wednesday, 6 August 2014 at 21:33:35 UTC, Timon Gehr wrote:
On 08/06/2014 11:18 PM, Matthias Bentrup wrote:
Ah, I had a different understanding of assume, i.e. placing an
assume(A) at some point in code adds not the axiom A, but
rather
the axiom "control flow reaches this spot => A".
(Your understanding is the conventional one.)
Not right.
You need to take into account that assume() provides a
mathematical definition, it isn't an imperative. That would make
no sense. So there is no control flow, only mathematical
dependencies.
You only deal with constants. "Variables" are just a tool for
automatic labeling of constants. You would not be able to use
logic otherwise.
"Control flow" is embedded in the dependencies and relationships
between the constants.
j=0
for(i=0; i<3;++i){j+=i}
Is just a short-hand for:
j0 = 0
i0 = 0
j1 = j0 + i0
i1 = 1
j2 = j1 + i1
i2 = 2
j3 = j2 + i2
If you map this out as a graph you get the dependencies
(mirroring "control flow").
Hoare-logic provide means to reason about the short-hand notation
and make transformations on it.
What is unconventional about this?
