The main goal here is to provide such specs for static analysis, because it's unclear how they'd be runtime checked.
This would allow specifying how items inside the module interact. Only need to support the maintains clause.
Together with quantifiers (forall and exists), it would allow e.g. characterizing algebraic structures such as groups, fields, vector spaces, etc.
The main goal here is to provide such specs for static analysis, because it's unclear how they'd be runtime checked.
This would allow specifying how items inside the module interact. Only need to support the
maintainsclause.Together with quantifiers (
forallandexists), it would allow e.g. characterizing algebraic structures such as groups, fields, vector spaces, etc.