pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Add missing "O - O = E" abstraction case

Browse source 
This case is implemented by parity_subtract in
AbstractInterpretation.v and is necessary to calculate the "most
precise abstraction."

See also #28, #37.
This commit is contained in:
Matthew Dempsky 2020-03-16 12:58:20 -07:00
parent 51a7fae33e
commit ebcd23ee6c
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
frap_book.tex
View file

@ -1984,6 +1984,7 @@ As an example, consider this formalization of even-odd analysis, whose proof of
\O \; \hat{+} \; \O &=& \E \\ \O \; \hat{+} \; \O &=& \E \\
\_ \; \hat{+} \; \_ &=& \top \\ \_ \; \hat{+} \; \_ &=& \top \\
\E \; \hat{-} \; \E &=& \E \\ \E \; \hat{-} \; \E &=& \E \\
\O \; \hat{-} \; \O &=& \E \\
\_ \; \hat{-} \; \_ &=& \top \\ \_ \; \hat{-} \; \_ &=& \top \\
\E \; \hat{\times} \; \_ &=& \E \\ \E \; \hat{\times} \; \_ &=& \E \\
\_ \; \hat{\times} \; \E &=& \E \\ \_ \; \hat{\times} \; \E &=& \E \\