Constant move_model::pragmas::CONDITION_ABSTRACT_PROP

pub const CONDITION_ABSTRACT_PROP: &str = "abstract";

Abstract property which can be used together with an opaque specification. An abstract property is not verified against the implementation, but will be used for the function’s behavior in the application context. This allows to “override” the specification with a more abstract version. In general we would need to prove the abstraction is subsumed by the implementation, but this is currently not done.