Quelle concfactorial.vdmpp Sprache: VDM

class Factorial
instance variables
result : nat := 5;

operations
public factorial : nat ==> nat
factorial(n) ==
  if n = 0 then return 1
  else (
   dcl m : Multiplier;
   m := new Multiplier();
   m.calculate(1,n);
   start(m);
   result:= m.giveResult();
   return result
  )

end Factorial

class Multiplier
instance variables
i : nat1;
j : nat1;
k : nat1;
result : nat1

operations
public calculate : nat1 * nat1 ==> ()
calculate (first, last) ==
  (i := first; j := last);

doit : () ==> ()
doit() ==
(
  if i = j then result := i
  else (
   dcl p : Multiplier;
   dcl q : Multiplier;
   p := new Multiplier();
   q := new Multiplier();
   start(p);start(q);
   k := (i + j) div 2;
   -- division with rounding down
   p.calculate(i,k);
   q.calculate(k+1,j);
   result := p.giveResult() * q.giveResult ()
  )
);

public giveResult : () ==> nat1
giveResult() ==
  return result;

sync
-- cyclic constraints allowing only the
-- sequence calculate; doit; giveResult

per doit => #fin (calculate) > #act(doit);
per giveResult => #fin (doit) > #act (giveResult);
per calculate => #fin (giveResult) = #act (calculate)

thread
doit();

end Multiplier

quality97%

¤ Dauer der Verarbeitung: 0.12 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.