Interface NNCalcController

All Known Implementing Classes:

NNCalcController1

public interface NNCalcController

Controller interface.

Mathematical Model (abstract value and abstract invariant of this):

type NNCalcController is modeled by
  (model: NNCalcModel,
   view: NNCalcView)

Constructor(s) (initial abstract value(s) of this):

(NNCalcModel model, NNCalcView view):
  ensures
    this.model = model  and
    this.view = view

Author:

Bruce W. Weide

Method Summary

Modifier and Type	Method and Description
void	processAddEvent() Processes event to do an add operation.
void	processAddNewDigitEvent(int digit) Processes event to add a new (low-order) digit to the bottom operand.
void	processClearEvent() Processes event to clear bottom operand.
void	processDivideEvent() Processes event to do a divide operation.
void	processEnterEvent() Processes event to enter bottom operand to top.
void	processMultiplyEvent() Processes event to do a multiply operation.
void	processPowerEvent() Processes event to do a power operation.
void	processRootEvent() Processes event to do a root operation.
void	processSubtractEvent() Processes event to do a subtract operation.
void	processSwapEvent() Processes event to swap operands.

Method Detail

processClearEvent

void processClearEvent()

Processes event to clear bottom operand.

Updates:

this.model.bottom, this.view

Ensures:

this.model.bottom = 0  and
[this.view has been updated to match this.model]

processSwapEvent

void processSwapEvent()

Processes event to swap operands.

Updates:

this.model, this.view

Ensures:

this.model.top = #this.model.bottom  and
this.model.bottom = #this.model.top  and
[this.view has been updated to match this.model]

processEnterEvent

void processEnterEvent()

Processes event to enter bottom operand to top.

Updates:

this.model.top, this.view

Ensures:

this.model.top = this.model.bottom  and
[this.view has been updated to match this.model]

processAddEvent

void processAddEvent()

Processes event to do an add operation.

Updates:

this.model, this.view

Ensures:

this.model.top = 0  and
this.model.bottom = #this.model.top + #this.model.bottom  and
[this.view has been updated to match this.model]

processSubtractEvent

void processSubtractEvent()

Processes event to do a subtract operation.

Updates:

this.model, this.view

Requires:

this.model.bottom <= this.model.top

Ensures:

this.model.top = 0  and
this.model.bottom = #this.model.top - #this.model.bottom  and
[this.view has been updated to match this.model]

processMultiplyEvent

void processMultiplyEvent()

Processes event to do a multiply operation.

Updates:

this.model, this.view

Ensures:

this.mode.top = 0  and
this.model.bottom = #this.model.top * #this.model.bottom  and
[this.view has been updated to match this.model]

processDivideEvent

void processDivideEvent()

Processes event to do a divide operation.

Updates:

this.model, this.view

Requires:

this.model.bottom > 0

Ensures:

#this.model.top =
  this.model.bottom * #this.model.bottom + this.model.top  and
0 <= this.model.top < #this.model.bottom  and
[this.view has been updated to match this.model]

processPowerEvent

void processPowerEvent()

Processes event to do a power operation.

Updates:

this.model, this.view

Requires:

this.model.bottom <= INT_LIMIT

Ensures:

this.model.top = 0  and
this.model.bottom = #this.model.top ^ (#this.model.bottom)  and
[this.view has been updated to match this.model]

processRootEvent

void processRootEvent()

Processes event to do a root operation.

Updates:

this.model, this.view

Requires:

2 <= this.model.bottom <= INT_LIMIT

Ensures:

this.model.top = 0  and
this.model.bottom =
  [the floor of the #this.model.bottom root of #this.model.top]  and
[this.view has been updated to match this.model]

processAddNewDigitEvent

void processAddNewDigitEvent(int digit)

Processes event to add a new (low-order) digit to the bottom operand.

Parameters:

digit - the low-order digit to be added

Updates:

this.model.bottom, this.view

Requires:

0 <= digit < 10

Ensures:

this.model.bottom = #this.model.bottom * 10 + digit  and
[this.view has been updated to match this.model]