Overture Tool

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