pub struct CheckedU16 { /* private fields */ }Expand description
This struct represents a $uty value that can overflow. The i field
is a ghost value that represents the true value, while the v field
is None when the value has overflowed and Some(x) when the value
x fits in a $uty.
Implementations§
Source§impl CheckedU16
impl CheckedU16
Sourcepub closed spec fn spec_new(v: u16) -> CheckedU16
pub closed spec fn spec_new(v: u16) -> CheckedU16
Creates a new $cty instance from a $uty value.
Ensures the internal representation matches the provided value.
Sourcepub exec fn new(v: u16) -> result : Self
pub exec fn new(v: u16) -> result : Self
result@ == v,Creates a new $cty instance from a $uty value.
Ensures the internal representation matches the provided value.
Sourcepub exec fn new_overflowed(Ghost(i): Ghost<int>) -> result : Self
pub exec fn new_overflowed(Ghost(i): Ghost<int>) -> result : Self
i > u16::MAX,result@ == i,Creates a new $cty instance with an overflowed value.
Requires the provided value to be greater than $uty::MAX.
Ensures the internal representation matches the provided value.
Sourcepub open spec fn spec_is_overflowed(&self) -> bool
pub open spec fn spec_is_overflowed(&self) -> bool
{ self@ > u16::MAX }Checks if the $cty instance is overflowed.
Returns true if the value is greater than $uty::MAX.
Sourcepub exec fn is_overflowed(&self) -> result : bool
pub exec fn is_overflowed(&self) -> result : bool
result == self.spec_is_overflowed(),Checks if the $cty instance is overflowed.
Returns true if the value is greater than $uty::MAX.
Sourcepub exec fn unwrap(&self) -> result : u16
pub exec fn unwrap(&self) -> result : u16
!self.is_overflowed(),result == self@,Unwraps the $cty instance to get the $uty value.
Requires the instance to not be overflowed.
Ensures the returned value matches the internal representation.
Sourcepub exec fn to_option(&self) -> result : Option<u16>
pub exec fn to_option(&self) -> result : Option<u16>
match result {
Some(v) => self@ == v && v <= u16::MAX,
None => self@ > u16::MAX,
},Converts the $cty instance to an Option<$uty>.
Ensures the returned option matches the internal representation.
Sourcepub exec fn add_value(&self, v2: u16) -> result : Self
pub exec fn add_value(&self, v2: u16) -> result : Self
result@ == self@ + v2,Adds a $uty value to the $cty instance.
Ensures the resulting value matches the sum of
the internal representation and the provided
value.
Sourcepub exec fn add_checked(&self, v2: &CheckedU16) -> result : Self
pub exec fn add_checked(&self, v2: &CheckedU16) -> result : Self
result@ == self@ + v2@,Adds another $cty instance to the current
instance. Ensures the resulting value matches
the sum of the internal representations of
both instances.
Sourcepub exec fn mul_value(&self, v2: u16) -> result : Self
pub exec fn mul_value(&self, v2: u16) -> result : Self
result@ == self@ as int * v2 as int,Multiplies the $cty instance by a $uty
value. Ensures the resulting value matches the
product of the internal representation and the
provided value.
Sourcepub exec fn mul_checked(&self, v2: &Self) -> result : Self
pub exec fn mul_checked(&self, v2: &Self) -> result : Self
result@ == self@ as int * v2@ as int,Multiplies the $cty instance by another $cty instance.
Ensures the resulting value matches the product of the internal
representations of both instances.