Wed, 27 Aug 2008 13:20:24 +0200

Related articles |
---|

Recognize valid paths plfriko@yahoo.de (Tim Frink) (2008-08-20) |

Re: Recognize valid paths m.helvensteijn@gmail.com (2008-08-23) |

Re: Recognize valid paths DrDiettrich1@aol.com (Hans-Peter Diettrich) (2008-08-24) |

Re: Recognize valid paths plfriko@yahoo.de (Tim Frink) (2008-08-26) |

Re: Recognize valid paths plfriko@yahoo.de (Tim Frink) (2008-08-26) |

Re: Recognize valid paths m.helvensteijn@gmail.com (Michiel Helvensteijn) (2008-08-27) |

Re: Recognize valid paths jeffrey.kenton@comcast.net (Jeff Kenton) (2008-09-01) |

From: | Michiel Helvensteijn <m.helvensteijn@gmail.com> |

Newsgroups: | comp.compilers |

Date: | Wed, 27 Aug 2008 13:20:24 +0200 |

Organization: | Wanadoo |

References: | 08-08-042 08-08-043 08-08-073 |

Keywords: | analysis |

Posted-Date: | 28 Aug 2008 10:05:59 EDT |

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

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.