Struct Positive 

pub struct Positive(/* private fields */);

Positive numbers, i.e. numbers that are strictly greater than 0.

Implementations

impl Positive

pub fn to_int(self) -> Int

logic

ensures

result > 0

pub fn new(n: Int) -> Self

logic

requires

n > 0

ensures

result.to_int() == n

pub fn ext_eq(self, other: Self) -> bool

logic(open)

let _ = Subset::<PositiveInner>::inner_inj;
self.to_int() == other.to_int()

ensures

#[trigger(self == other)] result == (self == other)

Trait Implementations

impl AddLogic for Positive

fn add_logic(self, other: Self) -> Self

logic

ensures

result@ == self@ + other@

type Output = Positive

impl Clone for Positive

fn clone(&self) -> Self

terminates

ghost

ensures

result == *self

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl MulLogic for Positive

fn mul_logic(self, other: Self) -> Self

logic

ensures

result@ == self@ * other@

type Output = Positive

impl OrdLogic for Positive

fn cmp_log(self, other: Self) -> Ordering

logic(open)

self.to_int().cmp_log(other.to_int())

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != core::cmp::Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == core::cmp::Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != core::cmp::Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == core::cmp::Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == core::cmp::Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == core::cmp::Ordering::Less

ensures

y.cmp_log(x) == core::cmp::Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == core::cmp::Ordering::Greater

ensures

y.cmp_log(x) == core::cmp::Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == core::cmp::Ordering::Equal)

fn le_log(self, o: Self) -> bool

The logical <= operation.

fn lt_log(self, o: Self) -> bool

The logical < operation.

fn ge_log(self, o: Self) -> bool

The logical >= operation.

fn gt_log(self, o: Self) -> bool

The logical > operation.

impl Plain for Positive

fn into_ghost(s: Snapshot<Self>) -> Ghost<Self>

terminates

ghost

ensures

*result == *s

impl RA for Positive

fn op(self, other: Self) -> Option<Self>

logic(open)

Some(self + other)

fn factor(self, factor: Self) -> Option<Self>

logic

ensures

match result {
    Some(c) => factor.op(c) == Some(self),
    None => forall<c: Self> factor.op(c) != Some(self),
}

fn commutative(a: Self, b: Self)

logic(law)

ensures

a.op(b) == b.op(a)

fn associative(a: Self, b: Self, c: Self)

logic

ensures

a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc))

fn core(self) -> Option<Self>

logic(open)

None

fn core_idemp(self)

logic

requires

self.core() != None

ensures

let c = self.core().unwrap_logic();
c.op(c) == Some(c)

ensures

self.core().unwrap_logic().op(self) == Some(self)

fn core_is_maximal_idemp(self, i: Self)

logic

requires

i.op(i) == Some(i)

requires

i.op(self) == Some(self)

ensures

match self.core() {
    Some(c) => i.incl(c),
    None => false,
}

fn cancelable(self) -> bool

logic(open)

let _ = Self::ext_eq;
true

ensures

result == (forall<x, y> self.op(x) != None ==>
    self.op(x) == self.op(y) ==> x == y)

fn eq(self, other: Self) -> bool

logic(open, inline)

fn incl(self, other: Self) -> bool

Inclusion of RA.

fn incl_op(self, other: Self, comb: Self)

logic(law)

fn incl_eq(self, other: Self) -> bool

logic(open, sealed)

fn incl_eq_op(a: Self, b: Self, x: Self) -> bool

logic(open, sealed)

fn update(self, x: Self) -> bool

Ensures that we can go from self to x without making composition with the frame invalid.

fn update_nondet(self, s: Set<Self>) -> bool

This is used in Resource::update_nondet.

fn associative_none(a: Self, b: Self, c: Self, bc: Self)

Specialized version of Self::associative, in the case where a.op(b) == None.

fn associative_some(a: Self, b: Self, c: Self, ab: Self, bc: Self)

Specialized version of Self::associative, in the case where a.op(b) and b.op(c) are both valid.

fn incl_transitive(a: Self, b: Self, c: Self)

RA::incl is transitive.

impl View for Positive

fn view(self) -> Int

logic(open)

self.to_int()

type ViewTy = Int

impl Copy for Positive