-
Notifications
You must be signed in to change notification settings - Fork 0
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Boogie Backend Redesign #153
Comments
Some observations from the move prover (see here):
See also this paper:
|
More thoughts:
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
(see also #72, #120 and #142)
This is an attempt to log the various problems with the current approach.
function
as a boogiefunction
is fraught with difficulties (why?). A better solution would be to translate them asprocedures
. This has a bunch of knock-on effects. In particular, we cannot use preconditions / postconditions inprocedures
. Instead, we must useassume
andassert
statements. Also, it means function calls have to be pulled out of expressions. In effect, we end up with something much closer to bytecode.procedure
is required for this.Vec
. See also Boogie Sequences #109. Questions remain around the heap and template.<A>[ref, Field A]A
for representing parts of the heap (seeMemory T
below). Boogie also has built-in support for "sequences" (see here), and supports tuple assignments.{:msg "your text goes here"}
The text was updated successfully, but these errors were encountered: