Interface AppendUndoController

public interface AppendUndoController

Controller interface.

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

 type AppendUndoController is modeled by
   (model: AppendUndoModel,
    view: AppendUndoView)
 

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

 (AppendUndoModel model, AppendUndoView view):
   ensures
     this.model = model  and
     this.view = view
 

Author:

Bruce W. Weide, Paolo Bucci

Method Summary

Methods

Modifier and Type	Method and Description
void	processAppendEvent(String input) Processes event to append to output.
void	processResetEvent() Processes event to reset model.
void	processUndoEvent() Processes event to undo last append to output.

Method Detail

processResetEvent

void processResetEvent()

Processes event to reset model.

Updates:

this.model, this.view

Ensures:

 this.model.input = ""  and
 this.model.output = <>  and
 [this.view has been updated to match this.model]
 

processAppendEvent

void processAppendEvent(String input)

Processes event to append to output.

Parameters:

input - string to be appended

Updates:

this.model, this.view

Ensures:

 this.model.input = ""  and
 this.model.output =  <input> * #this.model.output  and
 [this.view has been updated to match this.model]
 

processUndoEvent

void processUndoEvent()

Processes event to undo last append to output.

Updates:

this.model, this.view

Requires:

 this.model.output /= <>
 

Ensures:

 #this.model.output = <this.model.input> * this.model.output  and
 [this.view has been updated to match this.model]