public interface NNCalcModel
type NNCalcModel is modeled by
(top: NATURAL_NUMBER,
bottom: NATURAL_NUMBER)
():
ensures
this = (0, 0)
Modifier and Type | Method and Description |
---|---|
NaturalNumber |
bottom()
Reports bottom operand.
|
NaturalNumber |
top()
Reports top operand.
|
NaturalNumber top()
top
top = this.top
NaturalNumber bottom()
bottom
bottom = this.bottom