At the moment, it is hard to get a grasp of all assumptions that are made in any large verified codebase. We can easily find occurrences of assume, inhale, explicitly trusted functions and domain definitions, but searching for abstract predicates and methods/functions is a bit more annoying (can be done with regex though).
I would suggest requiring that all abstract members take the trusted annotation to make this easy to search for.
On a related note, @ArquintL and I once discussed the possibility of introducing a new kind of member (spec) for closure specifications, instead of using abstract methods. This would also make it clear that we are not introducing an assumption.
At the moment, it is hard to get a grasp of all assumptions that are made in any large verified codebase. We can easily find occurrences of
assume,inhale, explicitlytrustedfunctions anddomaindefinitions, but searching for abstract predicates and methods/functions is a bit more annoying (can be done with regex though).I would suggest requiring that all abstract members take the
trustedannotation to make this easy to search for.On a related note, @ArquintL and I once discussed the possibility of introducing a new kind of member (
spec) for closure specifications, instead of using abstract methods. This would also make it clear that we are not introducing an assumption.