Splitting 'and' conditions into multiple conditions 
Author Message
 Splitting 'and' conditions into multiple conditions

The simplifier is often unable to prove easy conclusions, because conditions
given als assert, precondition, and postcondition occur as a single
conclusion.

Example:
C1: res__1 >= buf__first and res__1 <= buf__last and (res__1 >= 0 and res__1
          <= 0) -> res__1 >= buf__first and res__1 <= buf__last .

Or do I misinterpret this line containing an implication?
Should the simplifier not able to handle this by transfering the frist part
to the hypothis?



Sun, 11 Sep 2005 05:48:33 GMT  
 Splitting 'and' conditions into multiple conditions

Quote:

> The simplifier is often unable to prove easy conclusions, because conditions
> given als assert, precondition, and postcondition occur as a single
> conclusion.

> Example:
> C1: res__1 >= buf__first and res__1 <= buf__last and (res__1 >= 0 and res__1
>      <= 0) -> res__1 >= buf__first and res__1 <= buf__last .

> Or do I misinterpret this line containing an implication?
> Should the simplifier not able to handle this by transfering the frist part
> to the hypothis?

Lutz,

We are always interested in collecting examples where the Simplifier can
be improved.  You should note, however, that the Simplifier is just
that, it is not intended to be a heavyweight proof engine like PVS.  The
idea is to limit what the Simplifier gets up to so as to maintain clear
traceability between what goes into it and what comes out and to avoid
the possibility of multiple substitutions leaving the formulae in a
worse state than they started.  The unsimplified VCs that are left can
always be tacked with the interactive Prof Checker tool.

Peter



Sun, 11 Sep 2005 17:41:24 GMT  
 
 [ 2 post ] 

 Relevant Pages 

1. oratcl - bind variable within 'in' condition

2. Order of evaluation of conditions in a combined condition

3. Order of evaluation of conditions in a combined condition/PMAP

4. Pre-condition vs. Post-condition

5. Pre-condition vs. Post-condition

6. Pre-condition vs Post-condition

7. "BIG E vs little e", was pre-condition vs post-condition

8. pre-condition vs post-condition

9. I have a 8+ Mb VI that won't save when in runnable condition

10. pitman's 2001 condition handling paper

11. probleme d'interpretation de ligne sur une condition

12. common action with multiple conditions

 

 
Powered by phpBB® Forum Software