[Civl] Add syntax for gates of actions

boogie-org / boogie

Boogie

MIT License

506 stars 111 forks source link

Closed shazqadeer closed 2 months ago

shazqadeer commented 2 months ago

This PR introduces new syntax for gates of atomic actions.

action Foo()
asserts g > 0;
{
...
}

Actions also support the requires and requires call annotations. Full support for these annotations will be added in a later PR.