Quelle Till.vdmpp Sprache: VDM

\section{The Class Till}

The Till class is virtually identical to the one presented in Appendix B
except that some of the operations have been modified to be able to deliver
the value <Fail> to represent failed communication with the CentralResource.
Also, the resource instance variable is now a reference to a LocalResource,
though since LocalResource and CentralResource have an identical calling
interface, this change is minimal. The remaining changes are self-explanatory,
so in the sequel we merely present the class, with any changes from the
previous version indicated by underlining.

\begin{vdm_al}
class Till

instance variables
  curCard : [Card] := nil;
  cardOk : bool := false;
  retainedCards : set of Card := {};
  resource : LocalResource;

  inv curCard = nil => not cardOk;

operations
  public Till: LocalResource ==> Till
  Till(res) ==
    resource := res;

  public Set: LocalResource ==> Till
  Set(res) ==
   (resource := res;
    return self);

  public InsertCard : Card ==> ()
  InsertCard(c) ==
    curCard := c
  pre not CardInside();

  public Validate : Card`PinCode ==> <PinOk> | <PinNotOk> | <Retained>
                              | <Fail>
  Validate(pin) ==
    let cardId = curCard.GetCardId(),
        codeOk = curCard.GetCode() = Encode(pin),
        cardLegal = IsLegalCard()
    in if cardLegal = <Fail>
       then return <Fail>
       else
          (cardOk := codeOk and cardLegal;
           if not cardLegal
           then (retainedCards := retainedCards union {curCard};
                 curCard := nil;
                 return <Retained>)
           elseif codeOk
           then if resource.ResetNumberOfTries(cardId) = <Fail>
                then return <Fail>
                else return <PinOk>
           else
             (let incTries = resource.IncrNumberOfTries(cardId),
                  numTriesExceeded =
                             resource.NumberOfTriesExceeded(cardId) in
              if <Fail> in set {incTries, numTriesExceeded}
              then return <Fail>
              elseif numTriesExceeded then
                (retainedCards := retainedCards union {curCard};
                 cardOk := false;
                 curCard := nil;
                 return <Retained>)
              else return <PinNotOk>
             )
          )
  pre CardInside() and not cardOk;

  public ReturnCard : () ==> ()
  ReturnCard() ==
    (cardOk := false;
     curCard:= nil)
  pre CardInside();

  public GetBalance : () ==> [nat]|<Fail>
  GetBalance() ==
    resource.GetBalance(curCard.GetAccountId())
  pre CardValidated();

  public MakeWithdrawal : nat ==> bool | <Fail>
  MakeWithdrawal(amount) ==
    resource.Withdrawal
      (curCard.GetAccountId(),curCard.GetCardId(),amount)
  pre CardValidated();

  public RequestStatement : () ==> bool | <Fail>
  RequestStatement() ==
    resource.PostStatement(curCard.GetAccountId(),curCard.GetCardId())
  pre CardValidated();
\end{vdm_al}

The IsLegalCard operation below is only used internally to validate a card.

\begin{vdm_al}
  public IsLegalCard : () ==> bool | <Fail>
  IsLegalCard() ==
    return
      resource.IsLegalCard(curCard.GetAccountId(),curCard.GetCardId())
  pre CardInside();

  pure public CardValidated: () ==> bool
  CardValidated() ==
    return curCard <> nil and cardOk;

  pure public CardInside: () ==> bool
  CardInside() ==
   return curCard <> nil;

functions

  Encode: Card`PinCode +> Card`Code
  Encode(pin) ==
    pin; -- NB The actual encoding procedure has not yet been chosen

end Till
\end{vdm_al}

quality83%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.