Re: Recognize valid paths

Tim Frink wrote:


> > if (x > 10)
> > assert( x > 10 && ((firstScope && x == 1) || (x >= 1 && !
> > firstScope)) );
> > // |
> > // V
> > assert( x > 10 && !firstScope);
> > x = 10;
> > }
>
> A question on this simplification after "->". What type of rules to
> do apply to infer that
> "((firstScope && x == 1) || (x >= 1 && ! firstScope)) )"
> becomes "!firstScope" ?


Ah, but you forget that we also know that "x > 10". I will give the
intermediate steps of the simplification:


x > 10 && ((firstScope && x == 1) || (x >= 1 && !firstScope))
        [&& distributivity]
(x > 10 && firstScope && x == 1) || (x > 10 && x >= 1 && !firstScope)
        ["x > 10 && x == 1" = "false"]
(false && firstScope) || (x > 10 && x >= 1 && !firstScope)
        ["x > 10" implies "x >= 1"]
(false && firstScope) || (x > 10 && !firstScope)
        ["false && B" = "false"]
false || (x > 10 && !firstScope)
        ["false || B" = "B"]
x > 10 && !firstScope


It's simplifications like this, and conclusions you can draw from it, that
require a sophisticated logic solver if you want to do this analysis
automatically. And such solvers cannot guarantee an answer and might run
indefinitely.


> > But if they're unclear, I can try to give an informal explanation.
>
> That would be fine.


I'm not an expert (yet), but I'll try to explain. You can only use the
simple version of the rules if no variable has any relation to any other
variable. Like in this example, x only has a relation with literal integers
and firstScope also stands on its own in the logical conjunctions. This is
a rule of thumb I came up with and I wouldn't count on it in the general
case. But the simple rules I used work like this:


spc(statement, pre) returns the strongest postcondition of statement, given
precondition pre.


wo(cond, a) returns "cond", but with all constraints on "a" removed.


For assignment:
spc("a = b;", pre) = ( wo(pre, a) && a == b )


For if-statements:
spc("if (c) S1; else S2;", pre) =
        ( spc(S1, pre && c) || spc(S2, pre && !c) )


For no-op (the empty operation):
spc(";", pre) = pre


For if-statements without else (using "else no-op;"):
spc("if (c) S1;", pre) = ( spc(S1, pre && c) || (pre && !c) )


There are similar rules for while-loops and such, but they're more
complicated.


> In general, how do you call this type of equations and their
> solving?


Not sure. Possibly "Strongest Postcondition Logic".


> Are there any known approaches for that?


Yes. But in general, you can't use the simple rules I just showed you. See
this example:


assert(1 <= a && a <= 10);
b = a + 1;
assert(1 <= a && a <= 10 && b == a + 1);
a = 20;
assert( ??? );


What's the strongest postcondition here? Following the simple rules, it
would either be (a == 20) or maybe (a == 20 && b == a + 1). Both are wrong.
The first gives no guarantees about b at all and the second gives the wrong
guarantee, since it uses the new value of a where it should use the old
one. The correct postcondition would be:


assert(a = 20 && 1 <= a_old && a_old <= 10 && b == a_old + 1);


You see? a_old is a logical variable I introduced to complete the assertion
correctly. A logical variable does not appear in the implementation and
only exists for the proof.


Have fun!


--
Michiel

Return to the comp.compilers page.
Search the comp.compilers archives again.