main
test-branch
| Line | |
|---|
| 1 |
|
|---|
| 2 | ACSL
|
|---|
| 3 |
|
|---|
| 4 | \forall decl_list ;
|
|---|
| 5 |
|
|---|
| 6 | QUANT DECLS SEMI FORMULA
|
|---|
| 7 |
|
|---|
| 8 |
|
|---|
| 9 | Q D ; p ==> q
|
|---|
| 10 | Q D ; (p ==> q)
|
|---|
| 11 |
|
|---|
| 12 | not: (Q D ; p) ==> q
|
|---|
| 13 |
|
|---|
| 14 | Similar: a+b*c is a+(b*c), not (a+b)*c
|
|---|
| 15 |
|
|---|
| 16 | (Q D ;)+ NOTQUANTFORM
|
|---|
| 17 |
|
|---|
| 18 |
|
|---|
| 19 |
|
|---|
| 20 | a && b || c should be (a && b) || c
|
|---|
| 21 |
|
|---|
| 22 | but
|
|---|
| 23 |
|
|---|
| 24 | a && Q D ; p || q is a && (Q D ; p || q)
|
|---|
| 25 |
|
|---|
| 26 |
|
|---|
| 27 | formula: quant | equiv
|
|---|
| 28 |
|
|---|
| 29 | quant: Q D ; form
|
|---|
| 30 |
|
|---|
| 31 | equiv: implies (<==> (quant | equiv))?
|
|---|
| 32 | implies: or (OR (quant | or))?
|
|---|
| 33 | or: and (AND (quant | and))?
|
|---|
| 34 | and: ...
|
|---|
Note:
See
TracBrowser
for help on using the repository browser.
