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()
toptop = this.topNaturalNumber bottom()
bottombottom = this.bottom