Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: abpursefunctional.vdmpp Sprache: VDM

Original von: VDM^©

class AbPurseFunctional

types

public AbPurse :: balance : nat
                   lost : nat;

public  PurseId = token;

public AbWorld ::
   authentic : set of PurseId
   abPurses : map PurseId to AbPurse
inv mk_AbWorld(authentic, abPurses) ==
  forall name in set dom abPurses &
       name in set authentic;

functions

public GetBalance: AbPurse -> nat
  GetBalance(p) == p.balance;

public GetLost: AbPurse -> nat
  GetLost(p) == p.lost;

public IncreaseBalance: AbPurse * nat -> AbPurse
  IncreaseBalance(p, val) ==
    mk_AbPurse(p.balance + val, p.lost);

public IncreaseLost: AbPurse * nat -> AbPurse
  IncreaseLost(p, val) ==
    mk_AbPurse(p.balance, p.lost + val);

public ReduceBalance: AbPurse * nat -> AbPurse
  ReduceBalance(p, val) ==
    mk_AbPurse(p.balance - val, p.lost)
  pre p.balance >= val;

public GetTotal : AbPurse -> nat
  GetTotal(p) ==
    p.balance + p.lost;

newAbWorld : map PurseId to AbPurse * set of PurseId -> AbWorld
  newAbWorld(purses, auth) ==
    mk_AbWorld(auth, purses)
  pre dom purses subset auth;

public TransferOk: AbWorld * PurseId * PurseId * nat -> AbWorld
  TransferOk(wrld, frm, too, val) ==
  (let
  newFrm =
   ReduceBalance(wrld.abPurses(frm),val),
  newTo =
   IncreaseBalance(wrld.abPurses(too),val)
  in
   mk_AbWorld(wrld.authentic,
     wrld.abPurses ++
       {frm |-> newFrm, too |-> newTo})
   )
  pre frm <> too and
    frm in set dom wrld.abPurses
    and
    too in set dom wrld.abPurses
    and
    (GetBalance(wrld.abPurses(frm)) >= val)
  post (GetTotal(RESULT.abPurses(frm)) +
    GetTotal(RESULT.abPurses(too)) =
  (GetTotal(wrld.abPurses(frm)) +
       GetTotal(wrld.abPurses(too)))
    and
(GetBalance(RESULT.abPurses(frm)) +
      GetBalance(RESULT.abPurses(too))) =
  (GetBalance(wrld.abPurses(frm)) +
       GetBalance(wrld.abPurses(too)))
    and
forall name in
     set (dom RESULT.abPurses) \ {frm, too}
     &
(GetBalance(wrld.abPurses(name)) =
      GetBalance(RESULT.abPurses(name)))
and
    (GetLost(wrld.abPurses(name)) =
      GetLost(RESULT.abPurses(name))));

public TransferLost: AbWorld * PurseId * PurseId * nat -> AbWorld
  TransferLost(wrld, frm, -, val) ==
  (
  let
   newFrm =
    ReduceBalance(wrld.abPurses(frm),val)
   in
   mk_AbWorld(wrld.authentic,
    wrld.abPurses ++
     {frm |-> IncreaseLost(newFrm, val)})
   )
  pre frm in set dom wrld.abPurses and
   GetBalance(wrld.abPurses(frm)) >= val
  post GetTotal(RESULT.abPurses(frm)) =
    GetTotal(wrld.abPurses(frm)) and
  GetBalance(wrld.abPurses(frm)) >=
    GetBalance(RESULT.abPurses(frm))
    and
forall name in
      set (dom RESULT.abPurses) \ {frm} &
    GetBalance(wrld.abPurses(name)) =
    GetBalance(RESULT.abPurses(name))
    and
  GetLost(wrld.abPurses(name)) =
      GetLost(RESULT.abPurses(name));

operations

public RunTest : () ==> AbWorld
RunTest () ==
  (let w : AbWorld = mk_AbWorld({mk_token(1), mk_token(2)},
                                {mk_token(1) |-> mk_AbPurse(100,0), mk_token(2) |-> mk_AbPurse(10,0)})
   in
     TransferOk(w, mk_token(1), mk_token(2), 30);
  );

end AbPurseFunctional

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.