pub enum Condition_ {
Ensures(SpecExp),
Requires(SpecExp),
AbortsIf(SpecExp),
SucceedsIf(SpecExp),
}
Expand description
A specification directive to be verified
Variants§
Ensures(SpecExp)
Postconditions
Requires(SpecExp)
Preconditions
AbortsIf(SpecExp)
If the given expression is true, the procedure must terminate in an aborting state
SucceedsIf(SpecExp)
If the given expression is true, the procedure must terminate in a succeeding state
Trait Implementations§
source§impl Clone for Condition_
impl Clone for Condition_
source§fn clone(&self) -> Condition_
fn clone(&self) -> Condition_
Returns a copy of the value. Read more
1.0.0 · source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source
. Read moresource§impl Debug for Condition_
impl Debug for Condition_
source§impl PartialEq<Condition_> for Condition_
impl PartialEq<Condition_> for Condition_
source§fn eq(&self, other: &Condition_) -> bool
fn eq(&self, other: &Condition_) -> bool
This method tests for
self
and other
values to be equal, and is used
by ==
.