viperproject / gobra-libs

Standard library for the Gobra verifier for Go. Contains definitions and lemmas useful for verifying large projects.
MIT License
2 stars 1 forks source link

Add initial sequences package + Make package names consistent #11

Closed dnezam closed 7 months ago

dnezam commented 9 months ago

Implements all definitions from Dafny that do not rely on any (multi)set-related definitions. These will be implemented using separate branches.

Additionally renames the packages to their singular form, and updates folder and file names for consistency.

dnezam commented 7 months ago

The following functions still have a quantifier in their postcondition:

Do we want to factor out these quantifiers like we did for IndexOf and IndexOfLast? Additionally, it may be useful to put the 2 quantifiers ensuring that a sequence is the same besides at one index into a separate function, since it is reused multiple times.