Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

SSlibE2PP

Author: Shin Sahara

This example contains a large collection of test classes that can be used to test different aspects of VDM++. This makes use of the VDMUnit test approach.

Properties Values
Language Version: classic
Entry point : new AllT().run()

FSequence.vdmpp

                                                                                                                                                                                                                                                                                                        
class FSequence
--"$Id: Sequence.vpp,v 1.1 2005/10/31 02:09:58 vdmtools Exp $";
	
functions 

                                                                     
static public Sum[@T] : seq of @T ->  @T
Sum(s) == Foldl[@T, @T](Plus[@T])(0)(s)
pre
	is_(s, seq of int) or is_(s, seq of nat) or is_(s, seq of nat1) or
 	is_(s, seq of real) or is_(s, seq of rat);
                                                                      
static public Prod[@T] : seq of @T ->  @T
Prod(s) == Foldl[@T, @T](Product[@T])(1)(s)
pre
	is_(s, seq of int) or is_(s, seq of nat) or is_(s, seq of nat1) or
 	is_(s, seq of real) or is_(s, seq of rat);
                                                       
static public Plus[@T] : @T -> @T -> @T
Plus(a)(b) == if is_real(a) and is_real(b)
              then a + b
              else undefined;
                                                         
static public Product[@T] : @T -> @T -> @T
Product(a)(b) == if is_real(a) and is_real(b)
              then a * b
              else undefined;
                                                              
static public Append[@T] : seq of @T -> @T -> seq of @T
Append(s)(e) == s ^ [e];
                                                                            
static public Average[@T]: seq of @T ->  [real]
Average(s) == if s = [] then nil else AverageAux[@T](0)(0)(s)
post
	if s = [] then
		RESULT = nil
	else let sum = Sum[@T](s)
	     in
		RESULT = if is_real(sum) 
		         then sum / len s
		         else undefined;

static AverageAux[@T] : @T -> @T -> seq of @T -> real
AverageAux(total)(numOfElem)(s) ==
  if is_(s,seq of real) and is_real(total) and is_real(numOfElem)
  then
	cases s :
	[x] ^ xs	-> AverageAux[@T](total + x)(numOfElem + 1)(xs),
	[]		-> total / numOfElem 
	end
	else undefined;
                                                                                                                                                      
static public IsAscendingInTotalOrder[@T] : (@T * @T -> bool) -> seq of @T -> bool
IsAscendingInTotalOrder(f)(s) ==
	forall i,j  in set inds s & i < j  => f(s(i),s(j)) or s(i) = s(j);
                                                                                                                                                       
static public IsDescendingInTotalOrder[@T] : (@T * @T -> bool) -> seq of @T -> bool
IsDescendingInTotalOrder(f)(s) ==
	forall i,j  in set inds s & i < j  => f(s(j),s(i)) or s(i) = s(j);
                                                                                                                                             
static public IsAscending [@T]: seq of @T -> bool
IsAscending(s) ==
	IsAscendingInTotalOrder[@T](lambda x : @T, y : @T & 
	                              if is_real(x) and is_real(y) 
	                              then x < y
	                              else undefined)(s);
                                                                                                                                              
static public IsDescending[@T]: seq of @T -> bool
IsDescending(s) ==
	IsDescendingInTotalOrder[@T](lambda x : @T, y : @T & 
	                                  if is_real(x) and is_real(y) 
	                                  then x < y
	                                  else undefined)(s);
                                                                                                                                   
static public Sort[@T] : (@T * @T -> bool) -> seq of @T -> seq of @T
Sort(f)(s) ==
	cases s:
		[]	-> [],
		[x]^xs	-> 
			Sort[@T](f)([xs(i) | i in set inds xs & f(xs(i),x)]) ^
			[x] ^
			Sort[@T](f)([xs(i) | i in set inds xs & not f(xs(i),x)])
	end;
                                                                                                                                   
static public AscendingSort[@T] : seq of @T -> seq of @T
AscendingSort(s) == Sort[@T](lambda x : @T, y : @T & 
                                if is_real(x) and is_real(y) 
	                              then x < y
	                              else undefined)(s)
post
	IsAscending[@T](RESULT);
                                                                                                                                                                       
static public DescendingSort[@T] : seq of @T -> seq of @T
DescendingSort(s) == Sort[@T](lambda x : @T, y : @T & 
                                  if is_real(x) and is_real(y) 
	                                then x > y
	                                else undefined)(s)
post
	IsDescending[@T](RESULT);
                                                                                                                                                 
static public IsOrdered[@T] : seq of (@T * @T -> bool) -> seq of @T -> seq of @T -> bool
IsOrdered(f)(s1)(s2) ==
	cases mk_(s1,s2):
		mk_([],[])			-> false,
		mk_([],-)			-> true,
		mk_(-,[])			-> false,
		mk_([x1]^xs1,[x2]^xs2)	->
			if (hd f)(x1,x2) then
				true
			elseif (hd f)(x2,x1) then
				false
			else
				IsOrdered[@T](tl f)(xs1)(xs2)
	end;
                                                                                                                   
static public Merge[@T] : (@T * @T -> bool) -> seq of @T -> seq of @T -> seq of @T
Merge(f)(s1)(s2) == 
	cases mk_(s1,s2):
		mk_([], y)			-> y,
		mk_(x, [])			-> x,
		mk_([x1]^xs1,[x2]^xs2)	->
			if f(x1,x2) then
				[x1] ^ FSequence`Merge[@T](f)(xs1)(s2)
			else
				[x2] ^ FSequence`Merge[@T](f)(s1)(xs2)
	end;
                                                                                                    
static public InsertAt[@T]: nat1 -> @T -> seq of @T -> seq of @T
InsertAt(i)(e)(s) ==
	cases mk_(i, s) :
	mk_(1, s1)		-> [e] ^ s1,
	mk_(-, [])		-> [e],
	mk_(i1, [x] ^ xs)	-> [x] ^ InsertAt[@T](i1 - 1)(e)(xs)
	end;
                                                                                                   
static public RemoveAt[@T]: nat1 -> seq of @T -> seq of @T
RemoveAt(i)(s) ==
	cases mk_(i, s) :
	mk_(1, [-] ^ xs)	-> xs,
	mk_(i1, [x] ^ xs)	-> [x] ^ RemoveAt[@T](i1 - 1)(xs),
	mk_(-, [])		-> []
	end;
                                                                                          
static public RemoveDup[@T] :  seq of @T ->  seq of @T
RemoveDup(s) == 
	cases s :
	[x]^xs		-> [x] ^ RemoveDup[@T](Filter[@T](lambda e : @T & e <> x)(xs)) ,
	[]		-> []
	end
post
	not IsDup[@T](RESULT);
                                                                                   
static public RemoveMember[@T] :  @T -> seq of @T -> seq of @T
RemoveMember(e)(s) == 
	cases s :
	[x]^xs		-> if e = x then xs else [x] ^ RemoveMember[@T](e)(xs),
	[]		-> []
	end;
                                                                                                    
static public RemoveMembers[@T] :  seq of @T -> seq of @T -> seq of @T
RemoveMembers(es)(s) == 
	cases es :
	[]		-> s,
	[x]^xs		-> RemoveMembers[@T](xs)(RemoveMember[@T](x)(s))
	end;
                                                                                                                                  
static public UpdateAt[@T]: nat1 -> @T -> seq of @T -> seq of @T
UpdateAt(i)(e)(s) ==
	cases mk_(i, s) :
	mk_(-, [])		-> [],
	mk_(1, [-] ^ xs)	-> [e] ^ xs,
	mk_(i1,  [x] ^ xs)	-> [x] ^ UpdateAt[@T](i1 - 1)(e)(xs)
	end;
                                                                                   
static public Take[@T] : int -> seq of @T -> seq of @T
Take(i)(s) == s(1,...,i);
                                                                                                                         
static public TakeWhile[@T] : (@T -> bool) -> seq of @T ->seq of @T
TakeWhile(f)(s) ==
	cases s :
	[x] ^ xs	-> 
		if f(x) then
			[x] ^ TakeWhile[@T](f)(xs)
		else
			[],
	[]	-> []
	end;
                                                                                
static public Drop[@T]: int -> seq of @T -> seq of @T
Drop(i)(s) == s(i+1,...,len s);
                                                                                                                      
static public DropWhile[@T] : (@T -> bool) -> seq of @T ->seq of @T
DropWhile(f)(s) ==
	cases s :
	[x] ^ xs	-> 
		if f(x) then
			DropWhile[@T](f)(xs)
		else
			s,
	[]	-> []
	end;
                                                                                                                                                                                         
static public Span[@T] : (@T -> bool) -> seq of @T -> seq of @T * seq of @T
Span(f)(s) ==
	cases s :
	[x] ^ xs	-> 
		if f(x) then
			let	mk_(satisfied, notSatisfied) = Span[@T](f)(xs)
			in
			mk_([x] ^ satisfied, notSatisfied)
		else
			mk_([], s),
	[]	-> mk_([], [])
	end;
                                                                                                                
static public SubSeq[@T]: nat -> nat -> seq1 of @T -> seq of @T
SubSeq(i)(numOfElems)(s) == s(i,...,i + numOfElems - 1);
                                                                         
static public Last[@T]: seq of @T -> @T
Last(s) == s(len s);
                                                                                          
static public Fmap[@T1,@T2]: (@T1 -> @T2) -> seq of @T1 -> seq of @T2
Fmap(f)(s) == [f(s(i)) | i in set inds s];
                                                                                                                                                                   
static public Filter[@T]: (@T -> bool) -> seq of @T -> seq of @T
Filter(f)(s) == [s(i) | i in set inds s & f(s(i))];
                                                                                                                    
static public Foldl[@T1, @T2] : (@T1 -> @T2 -> @T1) -> @T1 -> seq of @T2 -> @T1
Foldl(f)(args)(s) == 
	cases s :
	[]		-> args,
	[x] ^ xs	-> Foldl[@T1,@T2](f)(f(args)(x))(xs)
	end;
                                                                                                                      
static public Foldr[@T1, @T2] : 
	(@T1 -> @T2 -> @T2) -> @T2 -> seq of @T1 -> @T2
Foldr(f)(args)(s) == 
	cases s :
	[]		-> args,
	[x] ^ xs	-> f(x)(Foldr[@T1,@T2](f)(args)(xs))
	end;
                                                                               
static public IsMember[@T] : @T -> seq of @T -> bool
IsMember(e)(s) == 
	cases s :
	[x]^xs		-> e = x or IsMember[@T] (e)(xs),
	[]		-> false
	end;
                                                                                                             
static public IsAnyMember[@T]:  seq of @T -> seq of @T -> bool
IsAnyMember(es)(s) == 
	cases es :
	[x]^xs		->  IsMember[@T] (x)(s) or IsAnyMember[@T] (xs)(s) ,
	[]		-> false
	end;
                                                                                            
static public IsDup[@T] : seq of @T -> bool
IsDup(s) == not card elems s = len s
post
	if s = [] then 
		RESULT = false
	else
		RESULT = not forall i, j in set inds s & s(i) <> s(j) <=> i <> j ;
                                                                                                                                              
static public Index[@T]: @T -> seq of @T -> int
Index(e)(s) == 
	let	i = 0
	in
	IndexAux[@T](e)(s)(i);

static public IndexAux[@T] : @T -> seq of @T -> int -> int
IndexAux(e)(s)(i) ==
	cases s:
		[]		-> 0,
		[x]^xs		->
			if x = e then 
				i + 1
			else
				IndexAux[@T](e)(xs)(i+1)
	end;
                                                                                                                                     
static public IndexAll[@T] : @T -> seq of @T -> set of nat1
IndexAll(e)(s) == {i | i in set inds s & s(i) = e};
                                                                                                                             
static public Flatten[@T] : seq of seq of @T -> seq of @T
Flatten(s) == conc s;
                                                                                                 
static public Compact[@T] : seq of [@T] -> seq of @T
Compact(s) == [s(i) | i in set inds s & s(i) <> nil]
post
	forall i in set inds RESULT & RESULT(i) <> nil;
                                                                                                                                               
static public Freverse[@T] : seq of @T -> seq of @T
Freverse(s) == [s(len s + 1 -  i) | i in set inds s];
                                                                        
static public Permutations[@T]: seq of @T -> set of seq of @T
Permutations(s) == 
cases s:
	[],[-] -> {s},
	others -> dunion {{[s(i)]^j | j in set Permutations[@T](RemoveAt[@T](i)(s))} | i in set inds s} 
end
post
	forall x in set RESULT & elems x = elems s;
                                                                                                            
static public IsPermutations[@T]: seq of @T -> seq of @T -> bool
IsPermutations(s)(t) == 
	RemoveMembers[@T](s)(t) = [] and RemoveMembers[@T](t)(s) = [];
                                                                               
static public Unzip[@T1, @T2] : seq of (@T1 * @T2) -> seq of @T1 * seq of @T2
Unzip(s) ==
	cases s :
	[]			-> mk_([], []),
	[mk_(x, y)] ^ xs	->
		let	mk_(s1, t) = Unzip[@T1, @T2](xs)
		in
		mk_([x] ^ s1, [y] ^ t)
	end;
                                                                             
static public Zip[@T1, @T2] : seq of @T1 * seq of @T2 -> seq of (@T1 * @T2)
Zip(s1, s2) == Zip2[@T1, @T2](s1)(s2);
                                                                                                                                          
static public Zip2[@T1, @T2] : seq of @T1 -> seq of @T2 -> seq of (@T1 * @T2)
Zip2(s1)(s2) == 
	cases mk_(s1, s2) :
	mk_([x1] ^ xs1, [x2] ^ xs2)	-> [mk_(x1, x2)] ^ Zip2[@T1, @T2](xs1)(xs2),
	mk_(-, -)				-> []
	end;

end FSequence
                                                                         

Object.vdmpp

class Object
/*
作成者 = 佐原伸
作成日 = 2000年 8月 23日 
Responsibility
	オブジェクト共通の振る舞いを表す。

Abstract
	すべてのオブジェクトに共通な機能を定義する。
*/
	
functions 

public hashCode : () -> int
hashCode() == 1;

public equals : Object -> bool
equals(-) == true;

operations
public getContent : () ==> [seq of char | int]
getContent() == return 1374;	--meaningless value. so subclass must set.
			
end Object

Integer.vdmpp

class Integer

functions 

static public asString: int -> seq1 of char 
asString(i) == 
	if i < 0 then
		"-" ^ asStringAux(-i)
	else
		asStringAux(i) ;
		
static public asStringAux: nat -> seq1 of char 
asStringAux(n) == 
	let	r = n mod 10,
		q = n div 10
	in
		cases q:
			0		-> asChar(r),
			others	-> asStringAux(q) ^ asChar(r)
		end
	measure ndiv10;

static ndiv10 : nat +> nat
ndiv10(n) == n div 10;

-- Convert integer to COBOL type number string (like ZZZ9.ZZ). 
static public asStringZ: seq of char -> int -> seq1 of char 
asStringZ(cobolStrConversionCommand)(i) == 
	let	minusSymbol = '-'	in
	if i < 0 then
		if cobolStrConversionCommand(1) = minusSymbol then
			[minusSymbol] ^ asStringZAux(String`subStr(cobolStrConversionCommand,2,len cobolStrConversionCommand))(-i, true)
		else
			asStringZAux(cobolStrConversionCommand)(-i, true)
	else
		if cobolStrConversionCommand(1) = minusSymbol then
			asStringZAux(String`subStr(cobolStrConversionCommand,2,len cobolStrConversionCommand))(i, true)
		else
			asStringZAux(cobolStrConversionCommand)(i, true) ;
 		
 static public asStringZAux: seq of char -> nat * bool -> seq1 of char 
 asStringZAux(cobolStrConversionCommand)(n, wasZero) == 
  	let	cobolStrConversionCommandStrLen = len cobolStrConversionCommand,
  		cobolStrConversionCommandChar = cobolStrConversionCommand(cobolStrConversionCommandStrLen),
  		cobolStrConversionCommandStr = String`subStr(cobolStrConversionCommand,1,cobolStrConversionCommandStrLen - 1),
  		r = n mod 10,
  		q = n div 10,
  		isZero = r = 0 and wasZero and q <> 0 
  	in
  		cases cobolStrConversionCommandStr:
  			[]		-> asCharZ(cobolStrConversionCommandChar)(r, isZero),
  			others	-> 
  				asStringZAux(cobolStrConversionCommandStr)(q, isZero) ^ 
  				asCharZ(cobolStrConversionCommandChar)(r, isZero)
 		end;
--measure  length;

static length : seq of char -> nat * bool -> nat
length(cobolStrConversionCommand)(-, -) == len cobolStrConversionCommand;

static public asCharZ : char -> nat * bool ->  seq1 of char | bool
asCharZ(cobolStrConversionCommandChar)(n, wasZero) ==
	cases n:
		0	-> 
			if cobolStrConversionCommandChar in set {'z', 'Z'} and wasZero then
				"0"
			elseif cobolStrConversionCommandChar = '0'  or cobolStrConversionCommandChar = '9' then
				"0"
			else
				" ",	-- Don't deal with all cases of cobolStrConversionCommandChar
		1	-> "1",
		2	-> "2",
		3	-> "3",
		4	-> "4",
		5	-> "5",
		6	-> "6",
		7	-> "7",
		8	-> "8",
		9	-> "9",
		others	-> false
	end;

static public asChar : int -> seq1 of char | bool
asChar(i) ==
	cases i:
		0	-> "0",
		1	-> "1",
		2	-> "2",
		3	-> "3",
		4	-> "4",
		5	-> "5",
		6	-> "6",
		7	-> "7",
		8	-> "8",
		9	-> "9",
		others	-> false
	end;

static public GCD : nat -> nat -> nat
GCD(x)(y) == 
	if y = 0 then x else GCD(y)(x rem y);
--measure GCDMeasure;

static GCDMeasure : nat -> nat -> nat
GCDMeasure(x)(-) == x;

static public LCM : nat -> nat -> nat
LCM(x)(y) ==
	cases mk_(x, y) :
	mk_(-, 0)	-> 0,
	mk_(0, -)	-> 0,
	mk_(z, w)	-> (z / GCD(z)(w)) * w
	end;
			
end Integer

UseCalendar.vdmpp

class UseCalendar

instance variables
sJC : JapaneseCalendar :=  new JapaneseCalendar();

traces

S1 : 
	let y in set {2010,...,2012} in let m in set {1,...,12} in let d in set {1,...,31} in sJC.getDateFrom_yyyy_mm_dd(y, m, d).asString()

S2:
	let y in set {2010,...,2100} in sJC.getVernalEquinox(y).date2Str()

end UseCalendar

StringT.vdmpp

class StringT is subclass of TestDriver 
functions
public tests : () -> seq of TestCase
tests () == 
	[
	new StringT01(), new StringT02(), 
	new StringT03(), new StringT04(),
	new StringT05(), new StringT06(),
	new StringT07(), new StringT08(),
	new StringT09(), -- new StringT10(),
	new StringT11(), new StringT12(),
	new StringT13(), new StringT14()
	];
end StringT

class StringT01 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	c = new Character()	in
	return
		(
		c.isDigit('0') = true and
		c.isDigit('1') = true and
		c.isDigit('2') = true and
		c.isDigit('3') = true and
		c.isDigit('4') = true and
		c.isDigit('5') = true and
		c.isDigit('6') = true and
		c.isDigit('7') = true and
		c.isDigit('8') = true and
		c.isDigit('9') = true and
		c.isDigit('a') = false and
		c.asDigit('0') = 0 and
		c.asDigit('1') = 1 and
		c.asDigit('2') = 2 and
		c.asDigit('3') = 3 and
		c.asDigit('4') = 4 and
		c.asDigit('5') = 5 and
		c.asDigit('6') = 6 and
		c.asDigit('7') = 7 and
		c.asDigit('8') = 8 and
		c.asDigit('9') = 9 and
		c.asDigit('a') = false )
;
protected setUp: () ==> ()
setUp() == TestName := "StringT01:\tConvert digit to integer.";
protected tearDown: () ==> ()
tearDown() == return;
end StringT01

class StringT02 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	c = new Character()	in
	return
		(c.asDictOrder('0') = 1 and
		c.asDictOrder('9') = 10 and
		c.asDictOrder('a') = 11 and
		c.asDictOrder('A') = 12 and
		c.asDictOrder('z') = 61 and
		c.asDictOrder('Z') = 62 and
		c.asDictOrder('\n') = 999999 and
		c.asDictOrder('\t') = 999999 )
;
protected setUp: () ==> ()
setUp() == TestName := "StringT02:\tReturn dictionary order of character.";
protected tearDown: () ==> ()
tearDown() == return;
end StringT02

class StringT03 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	s = new String(),
		LT = String`LT2,
		LE = String`LE2,
		GT = String`GT2,
		GE = String`GE2
	in
	return
		(s.LT("123","123") = false and
		LT("123")("123") = false and
		s.GT("123","123") = false and
		GT("123")( "123") = false and
		s.LT("","") = false and
		s.GT("","") = false and
		s.LT("","123") = true and
		s.GT("","123") = false and
		s.LT("123","") = false and
		s.GT("123","") and
		s.LT("123","1234") and
		s.GT("123","1234") = false and
		s.LT("1234","123") = false and
		s.GT("1234","123") and
		s.LT("123","223") and
		s.GT("123","223") = false and
		s.LE("123","123") and
		LE("123")("123") and
		s.GE("123","123") and
		s.LE("123","1234") and
		LE("123")("1234") and
		s.GE("123","1234") = false and
		GE("123")("1234") = false and
		s.LE("1234","123") = false and
		not LE("1234")("123") and
		s.GE("1234","123") and
		s.LE("","") and
		LE("")("") and
		Sequence`fmap[seq of char, bool](LT("123"))(["123", "1234", "", "223"]) = [false, true, false, true] and
		Sequence`fmap[seq of char, bool](LE("123"))(["1234", ""]) = [true, false] and
		Sequence`fmap[seq of char, bool](GT("123"))([ "123", "", "23"]) = [false, true, false] and
		Sequence`fmap[seq of char, bool](GE("123"))(["1234", ""]) = [false, true] 
		)
;
protected setUp: () ==> ()
setUp() == TestName := "StringT03:\tCompare magnitude of string.";
protected tearDown: () ==> ()
tearDown() == return;
end StringT03

class StringT04 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	s1234 = "1234",
		s = new String()	in
	return
		s1234 = "1234" and
		s.isSpaces("") = true and
		s.isSpaces("  ") = true and
		s.isSpaces(" \t  ") = true and
		s.isSpaces([]) = true 
;
protected setUp: () ==> ()
setUp() == TestName := "StringT04:\tCompare 2 strings is equal.";
protected tearDown: () ==> ()
tearDown() == return;
end StringT04

class StringT05 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	LT = Character`LT,
		GT = Character`GT,
		LE = Character`LE,
		GE = Character`GE
	in
	return
		(LT('a','a') = false and
		Character`LT2('a')('a') = false and
		GT('a','a') = false and
		Character`GT2('a')('a') = false and
		LT('1','2') and
		Character`LT2('1')('2') and
		GT('1','0') and
		Character`GT2('1')('0') and
		LT('9','a') and
		Character`LT2('9')('a') and
		GT('\n','0') and
		Character`GT2('\n')('0') and
		LE('a','0') = false and
		Character`LE2('a')('0') = false and
		GE('a','0') and
		Character`GE2('a')('0') and
		Sequence`fmap[char, bool](Character`LT2('5'))("456") = [false, false, true]
		)
;
protected setUp: () ==> ()
setUp() == TestName := "StringT05:\tCompare magnitude of character.";
protected tearDown: () ==> ()
tearDown() == return;
end StringT05

class StringT06 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	s = new String(),
		substr = String`SubStr
	in
	return
		(s.subStr("Shin Sahara",6,6) = "Sahara" and
		s.subStr("Shin Sahara",6,8) = "Sahara" and
		s.subStr("Shin Sahara",6,3) = "Sah" and
		s.subStr("Shin Sahara",1,0) = "" and
		s.subStrFill("sahara",1,3,'*') = "sah" and
		s.subStrFill("sahara",1,6,'*') = "sahara" and
		s.subStrFill("sahara",1,10,'*') = "sahara****" and
		s.subStrFill("sahara",3,4,'*') = "hara" and
		s.subStrFill("sahara",3,10,'*') = "hara******" and
		s.subStrFill("sahara",1,0,'*') = "" and
		s.subStrFill("",1,6,'*') = "******" and
		String`SubStr(6)(6)("Shin Sahara") = "Sahara" and
		substr(6)(8)("Shin Sahara") = "Sahara" and
		Sequence`fmap[seq of char, seq of char](substr(6)(8))(["1234567890", "12345671"]) = ["67890", "671"]
		)
;
protected setUp: () ==> ()
setUp() == TestName := "StringT06:\tGet substring.";
protected tearDown: () ==> ()
tearDown() == return;
end StringT06


class StringT07 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	return
		(String`isDigits("1234567890")  = true and
		String`asInteger("1234567890")  = 1234567890 and
		String`asInteger("")  = 0 
		)
;
protected setUp: () ==> ()
setUp() == TestName := "StringT07:\tHandling digit strings.";
protected tearDown: () ==> ()
tearDown() == return;
end StringT07

class StringT08 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	return
		(
		String`index("1234567890",'1')  = 1 and
		String`index("1234567890",'0') = 10 and
		String`index("1234567890",'a')  = 0 and
		String`indexAll("1234567890",'1')  = {1} and
		String`indexAll("1234567890",'0') = {10} and
		String`indexAll("1234567890",'a')  = {} and 
		String`indexAll("1231567190",'1')  = {1,4,8} and 
		String`indexAll("1231567191",'1')  = {1,4,8,10} and
		String`Index('1')("1234567890")  = 1 and
		String`Index('0')("1234567890") = 10 and
		String`Index('a')("1234567890")  = 0 and
		String`IndexAll2('1')("1234567890")  = {1} and
		String`IndexAll2('0')("1234567890") = {10} and
		String`IndexAll2('a')("1234567890")  = {} and 
		String`IndexAll2('1')("1231567190")  = {1,4,8} and 
		String`IndexAll2('1')("1231567191")  = {1,4,8,10} and
		Sequence`fmap[seq of char, int](String`Index('1'))(["1234567890", "2345671"]) = [1, 7] and
		Sequence`fmap[seq of char, set of int](String`IndexAll2('1'))(["1231567190", "1231567191"]) = [{1,4,8}, {1,4,8,10}]
		)
;
protected setUp: () ==> ()
setUp() == TestName := "StringT08:\tGet first position of a character in a string.";
protected tearDown: () ==> ()
tearDown() == return;
end StringT08

class StringT09 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let isInclude = String`isInclude
	in
	return
		(String`isInclude("1234567890")( "abc")  = false and
		isInclude("Shin")("Shin") = true and
		isInclude("Shin")("S") = true and
		isInclude("Shin")("h") = true and
		isInclude("Shin")("n") = true
		)
;
protected setUp: () ==> ()
setUp() == TestName := "StringT09:\tIs a string the substring of another string.";
protected tearDown: () ==> ()
tearDown() == return;
end StringT09

class StringT10 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
		tixe {<RuntimeError>  |->  return true } in
		return String`isInclude("Shin Sahara")("")
;
protected setUp: () ==> ()
setUp() == TestName := "StringT10:\tIs a string the substring of another string. In case of pre-condition error";
protected tearDown: () ==> ()
tearDown() == return;
end StringT10

class StringT11 is subclass of TestCase
operations 
public test: () ==> bool
test() == 
	return 
		let 区切り文字 = elems "\t\n " in
		String`GetToken("sahara\tshin", 区切り文字) = "sahara" and
		String`GetToken("sahara\tshin SCSK", 区切り文字) = "sahara" and
		String`DropToken("sahara\tshin", 区切り文字) = "\tshin" and
		String`DropToken("sahara\tshin SCSK", 区切り文字) = "\tshin SCSK" and
		String`DropToken("sahara\tshin SCSK\n", 区切り文字) = "\tshin SCSK\n"
;
protected setUp: () ==> ()
setUp() == TestName := "StringT11:\t指定した文字列の先頭tokenを得る。";
protected tearDown: () ==> ()
tearDown() == return;
end StringT11

/*
シナリオID
	文字列を行に分解するシナリオ
内容
	文字列を行に分解するかを検査する。
*/
class StringT12 is subclass of TestCase
operations 
public test: () ==> bool
test() == 
	return 
		let 対象文字列1 = "private 次状態を得る : () ==> 「状態」\n次状態を得る(aガード, aガード引数, aイベント, aイベント引数,  a処理時間) == (\ncases mk_(aガード, 現在状態, aイベント)  :\n\tmk_(-,-,(エラー検知)) -> return エラー中,\n",
			ss1 = String`getLines(対象文字列1),
			対象文字列2 = "佐原\n伸",
			ss2 = String`getLines(対象文字列2)
		in
		ss1(1) = "private 次状態を得る : () ==> 「状態」" and
		ss1(2) = "次状態を得る(aガード, aガード引数, aイベント, aイベント引数,  a処理時間) == (" and
		ss1(3) = "cases mk_(aガード, 現在状態, aイベント)  :" and
		ss1(4) = "\tmk_(-,-,(エラー検知)) -> return エラー中," and
		ss2(1) = "佐原" and
		ss2(2) = "伸"
;
protected setUp: () ==> ()
setUp() == TestName := "StringT12:\t文字列を行に分解する。";
protected tearDown: () ==> ()
tearDown() == return;
end StringT12

/*
シナリオID
	英数字か判定するシナリオ
内容
	英数字か判定が正しいかを検査する。
*/
class StringT13 is subclass of TestCase
operations 
public test: () ==> bool
test() == 
	return 
		let	w英字列 = "aAbBcCdDeEfFgGhHiIjJkKlLmMnNoOpPqQrRsStTuUvVwWxXyYzZ",
			w数字列 = "0123456789",
			w英数字列 = w英字列 ^ w数字列
		in
		String`isLetters(w英字列) and
		not String`isLetters(" " ^ w英字列) and
		String`isDigits(w数字列) and
		not String`isDigits(" " ^ w数字列) and
		not String`isDigits("a" ^ w数字列) and
		String`isLetterOrDigits(w英数字列)  and
		not String`isLetterOrDigits(w英数字列 ^ " ") 
;
protected setUp: () ==> ()
setUp() == TestName := "StringT13:\t英数字かの判定が正しいかを検査する。";
protected tearDown: () ==> ()
tearDown() == return;
end StringT13

class StringT14 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	isSomeString = String`isSomeString
	in	return 
		isSomeString(Character`isLetterOrDigit)("007isTheMmurder") and
		not isSomeString(Character`isLetterOrDigit)("007 is the mmurder") and
		isSomeString(Character`isCapitalLetter)("SAHARA") and
		not isSomeString(Character`isCapitalLetter)("Sahara") and
		isSomeString(Character`isLowercaseLetter)("sahara") and
		not isSomeString(Character`isLowercaseLetter)("Sahara") 
		
;
protected setUp: () ==> ()
setUp() == TestName := "StringT11:\tIs a some kind of string?";
protected tearDown: () ==> ()
tearDown() == return;
end StringT14

UniqueNumberT.vdmpp

class UniqueNumberT is subclass of TestDriver
functions
public tests : () -> seq of TestCase
tests () == 
	[new UniqueNumberT01()
	];
end UniqueNumberT

class UniqueNumberT01 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	o = new UniqueNumber()	in
	return
		(
		o.getUniqNumStr(1) = "1" and
		o.getUniqNumStr(1) = "2" and
		o.getUniqNumStr(1) = "3" and
		o.getUniqNumStr(1) = "4" and
		o.getUniqNumStr(1) = "5" and
		o.getUniqNumStr(1) = "6" and
		o.getUniqNumStr(1) = "7" and
		o.getUniqNumStr(1) = "8" and
		o.getUniqNumStr(1) = "9" and
		o.getUniqNumStr(1) = "1" and 
		o.getUniqNumStr(1) = "2" and
		o.getUniqNumStr(2) = "3" and
		o.getUniqNumStr(2) = "4" and
		o.getUniqNumStr(2) = "5" and
		o.getUniqNumStr(2) = "6" and
		o.getUniqNumStr(2) = "7" and
		o.getUniqNumStr(2) = "8" and
		o.getUniqNumStr(2) = "9" and
		o.getUniqNumStr(2) = "10" and 
		o.getUniqNumStr(2) = "11"
		)
;
protected setUp: () ==> ()
setUp() == TestName := " UniqueNumberT01:\t UniqueNumberT01 Unit test";
protected tearDown: () ==> ()
tearDown() == return;
end UniqueNumberT01

Calendar.vdmpp

class CalendarDefinition
values
	public homedir = ".";
types
	public NameOfDayOfTheWeek = <Mon> | <Tue> | <Wed> | <Thu> | <Fri> | <Sat> | <Sun>;
	public NumberOfDayOfTheWeek = nat
	inv d == d <= 6;	--number of day of the week (Sunday=0, Saturday=6);
	
end CalendarDefinition
--------------------------------------------------------------
class Calendar is subclass of CalendarDefinition	-- Gregorio Calendar
/*
Responsibility
	I am a Gregorio Calendar.
Abstract
	I calculate Gregorio Calendar by cooperating with Date class.
	You can get the the vernal equinox and the autumnal equinox until year 2099.
	My subclass has to define the set of holiday.
	My calculation is based on GMT, so my subclass has to calculate the diofference to GMT.
*/

values
	--difference of julianDate and modifiedJulianDate
	private daysDifferenceOfModifiedJulianDate = 2400000.5;

	private namesOfDayOfTheWeek = [<Sun>,<Mon>,<Tue>,<Wed>,<Thu>,<Fri>,<Sat>];

	private daysInYear = 365.25;
	protected monthsInYear = 12;
	private correctedMonths = 14;
	private daysInWeek = 7;
	private averageDaysInMonth = 30.6001;
	private yearInCentury = 100;
	private calculationCoefficientOfDate = 122.1;
	private calculationCoefficientOfYear = 4800;
	private centuryCalculationCoefficient = 32044.9;
	private theDayBeforeGregorioCalendarStarted  = 2299160.0;
	private theFirstDayOfGregorioCalendar  = 1582.78;
	
	io = new IO();

instance variables

	protected differenceWithGMT : real := 0;
	protected iToday : [Date] := nil;
	protected Year2Holidays : map int to set of Date := { |-> };	-- { year |-> set of holidays }

functions

----Comparing magnitude functions

public LT: Date * Date -> bool
LT(date1, date2) == date1.getModifiedJulianDate() < date2.getModifiedJulianDate();

public GT: Date * Date -> bool
GT(date1,date2) == date1.getModifiedJulianDate() > date2.getModifiedJulianDate();

public LE: Date * Date -> bool
LE(date1,date2) == not GT(date1,date2);

public GE: Date * Date -> bool
GE(date1,date2) == not LT(date1,date2);

-- Is date1 value equal date2 value?
public EQ: Date * Date -> bool
EQ(date1,date2) == date1.getModifiedJulianDate() = date2.getModifiedJulianDate();

public min : Date -> Date -> Date
min(date1)(date2) == if date1.LT(date2) then date1 else date2;

public max : Date -> Date -> Date
max(date1)(date2) == if date1.GT(date2) then date1 else date2;

----Query

public isDateString : 
	seq of char	-- date string (yyyymmdd format)
	->
	bool		-- if correct date then true else false
isDateString(yyyymmdd) == if getDateFromString(yyyymmdd) = false then false else true;

-- is leap year?
public isLeapYear: 
	int	-- year
	-> 
	bool	-- leap year or not
isLeapYear(year) == year mod 400 = 0 or (year mod yearInCentury <> 0 and year mod 4 = 0);

public getNumberOfDayOfTheWeek: Date -> NumberOfDayOfTheWeek
getNumberOfDayOfTheWeek(date) == 
	let	modifiedJulianDate = floor(date.getModifiedJulianDate())
	in	(modifiedJulianDate - 4) mod daysInWeek;

public getYyyymmdd: Date -> int * int * int
getYyyymmdd(date) == mk_(Year(date),Month(date),day(date));

public getNameOfDayOfTheWeek : Date -> NameOfDayOfTheWeek
getNameOfDayOfTheWeek(date) == namesOfDayOfTheWeek(getNumberOfDayOfTheWeek(date) + 1);

public getNumberOfDayOfTheWeekFromName : NameOfDayOfTheWeek -> NumberOfDayOfTheWeek
getNumberOfDayOfTheWeekFromName(nameOfDayOfTheWeek) == Sequence`Index[Calendar`NameOfDayOfTheWeek](nameOfDayOfTheWeek)(namesOfDayOfTheWeek) - 1;

public firstDayOfTheWeekInMonth : int * int * NameOfDayOfTheWeek -> Date
firstDayOfTheWeekInMonth(year, month,nameOfDayOfTheWeek) ==
	let	numberOfDayOfTheWeek = getNumberOfDayOfTheWeekFromName(nameOfDayOfTheWeek),
		firstDayOfMonth = getFirstDayOfMonth(year, month),
		diff = numberOfDayOfTheWeek - getNumberOfDayOfTheWeek(firstDayOfMonth) in
	cases true:
		(diff = 0)	-> firstDayOfMonth,
		(diff > 0)	-> firstDayOfMonth.plus(diff),
		(diff < 0)	-> firstDayOfMonth.plus((daysInWeek + diff) mod daysInWeek)
	end;

-- Get the last date which has the specified name of day of the week
-- My algorithm thinks "year Y, month 13" = "year y+1, month 1", so I can month + 1
public lastDayOfTheWeekInMonth : int * int *	NameOfDayOfTheWeek -> Date
lastDayOfTheWeekInMonth(year, month, nameOfDayOfTheWeek) == firstDayOfTheWeekInMonth(year,(month+1),nameOfDayOfTheWeek).minus(daysInWeek);

-- Get the n-th day of the week of specified month
public getNthDayOfTheWeek : int * int * int * NameOfDayOfTheWeek
	->
	Date | bool 	-- the date which has n-th  day of the week, if not exist then false
getNthDayOfTheWeek(aYear, aMonth, n, nameOfDayOfTheWeek) ==
	let	firstDayOfMonth = firstDayOfTheWeekInMonth(aYear,aMonth,nameOfDayOfTheWeek),
		r = firstDayOfMonth.plus(daysInWeek * (n - 1)) in
	cases Month(r):
		(aMonth)	-> r,
		others	-> false
	end;

--new Calendar().getFirstDayOfMonth(2001,7).get_yyyy_mm_dd() = mk_( 2001,7,1 )
public getFirstDayOfMonth : int * int -> Date
getFirstDayOfMonth(year, month) == getRegularDate(year, month, 1);

--new Calendar().getLastDayOfMonth(2001,7).get_yyyy_mm_dd() = mk_( 2001,7,31 )
public getLastDayOfMonth : int * int -> Date
getLastDayOfMonth(year, month) == getRegularDate(year, month+1, 1).minus(1);
	
public isSunday : Date -> bool
isSunday(date) == getNumberOfDayOfTheWeek(date) = 0;

public isSaturday : Date -> bool
isSaturday(date) == getNumberOfDayOfTheWeek(date) = 6;

public isWeekday : Date -> bool
isWeekday(date) == getNumberOfDayOfTheWeek(date) in set {1,...,5};

public isNotDayOff : Date -> bool
isNotDayOff(date) == not isSundayOrDayoff(date);

public isWeekday : NameOfDayOfTheWeek -> bool
isWeekday(nameOfDayOfTheWeek) == nameOfDayOfTheWeek not in set {<Sat>,<Sun>};

-- Return how many days between date1 and date2 of nameOfDayOfTheWeek.  
-- include date1 and date2 iff they have the nameOfDayOfTheWeek.
public getNumberOfTheDayOfWeek: Date * Date * NameOfDayOfTheWeek -> int
getNumberOfTheDayOfWeek(date1,date2,nameOfDayOfTheWeek) ==
	let	numberOfDayOfTheWeek = getNumberOfDayOfTheWeekFromName(nameOfDayOfTheWeek),
		startDate = min(date1)(date2),
		endDate = max(date1)(date2),
		numOfDays = diffOfDates(endDate,startDate) + 1,
		quotient = numOfDays div daysInWeek,
		remainder = numOfDays mod daysInWeek,
		delta = if subtractDayOfTheWeek(numberOfDayOfTheWeek,getNumberOfDayOfTheWeek(startDate)) + 1 <= remainder then 1 else 0	in
	quotient + delta
/*
post
	let	startDate = min(date1)(date2),
		endDate = max(date1)(date2)	in
	let setOfTheDayOfTheWeek = {day | day : Date & nameOfDayOfTheWeek = getNameOfDayOfTheWeek(day )}  in
	forall Date0, Date1  in set setOfTheDayOfTheWeek &
		startDate.LE(Date0) and Date0.LE(Date1) and Date1.LE(endDate) =>
			diffOfDates(Date1, Date0) mod 7 = 0 and 
	exists1 日i  in set setOfTheDayOfTheWeek &
		diffOfDates(日i, startDate) < 6 and
		exists1 日j  in set setOfTheDayOfTheWeek &
			diffOfDates(endDate, 日j) < 6 and
			diffOfDates(日j, 日i) = 7 * ((card setOfTheDayOfTheWeek) - 1)
*/
		;
/*
Following Japanese statement are the refinement proof by Shin Sahara and Mr. Toshiharu Yamazaki.
以下は、上記関数の山崎利治さんによる段階的洗練を佐原が「翻訳」した記述

pre
type R = {|rng [n → n / 7 | n∈Int]|} 	-- 7で割った商の集合
f, t∈Int, w∈R, 0≦f≦t,
h: Int → R 		--環準同型(ring homomorphism)

post
S = dom h(w) ∩ {f..t}・RESULT ≡ card(S) 	-- RESULTが答え (dom h(w)≡h-1(w))

--整数系を環(ring)と見て、その商環(quotient ring)への準同型写像があり、その代数系上で事後条件を満たすプログラムを作る
I ={f..t}
d = t - f + 1 	-- = card(I)
q = d / 7
r = d \ 7 		--7で割った余り

とすると、

q ≦ A ≦ q+1

が成り立つ。なぜなら、

任意の連続する7日間には、必ずw曜日がちょうど1日存在する。
card(I) = 7×q + r (0≦r<7)であるから、Iには少なくともq個の連続する7日間が存在するが、q+1個は存在しない。
余りのr日間にw曜日が存在するかも知れない。

次に、

x ++ y = (x + y) \ 7
x ┴ y = max(x - y, 0)
として、

T = {h(f)..h(f) ++ (r ┴ 1)}
を考える。Tは余りr日間の曜日に対応する(card(T) = r)。
すると、

A ≡ if w∈T then q + 1 els q end

ここで、

x minus y = if x ≧ y then x - y els x - y + 7 end
とすれば、

w∈T ⇔ (w minus h(f)) + 1 ≦ r
である。なぜならば

w∈T	⇔ {0..(r ┴ 1)}∋wユ = w minus h(f)
	⇔ r ┴ 1 ≧ wユ
	⇔ r ≧ (w minus h(f)) + 1

従って、プログラムは以下のようになる。

A(f, t w)≡
	let
		d ≡ t - f + 1
		q ≡ d / 7
		r ≡ d \ 7
		delta ≡ if (w minus h(f)) + 1 ≦ r then 1 els 0 end
		x minus y ≡ if x ≧ y then x - y els x - y + 7 end
	in
		q + delta
	end
*/

private subtractDayOfTheWeek: int * int -> int
subtractDayOfTheWeek(x,y) == if x >= y then x - y else x - y + daysInWeek;

--dateから、そのdateの属するyearを求める。
public Year: Date -> int
Year(date) ==
if monthAux(date) < correctedMonths then
		yearAux(date) - calculationCoefficientOfYear
	else
		yearAux(date) - calculationCoefficientOfYear + 1;
		
--dateから、そのdateの属するmonthを求める。
public Month: Date -> int
Month(date) == if monthAux(date) < correctedMonths then
		monthAux(date) - 1
	else
		monthAux(date) - 13;
		
--dateから、dayを求める。
public day: Date -> int
day(date) == daysFromTheBeginningOfTheMonth(date);

--new Date().daysFromNewYear(getDateFrom_yyyy_mm_dd(2001,12,31)) = 365
public daysFromNewYear: Date -> int
daysFromNewYear(date) == 
	let	firstDateOfYear = getDateFrom_yyyy_mm_dd(Year(date), 1, 0)
	in	diffOfDates(date,firstDateOfYear);

daysFromTheBeginningOfTheMonth: Date -> int
daysFromTheBeginningOfTheMonth(date) == floor(daysFromTheBeginningOfTheMonthAsReal(date));

daysFromTheBeginningOfTheMonthAsReal: Date -> real
daysFromTheBeginningOfTheMonthAsReal(date) == yyyymmddModifyAux(date) + calculationCoefficientOfDate
- floor(daysInYear * yearAux(date)) - floor(averageDaysInMonth * monthAux(date)); 

monthAux: Date -> int
monthAux(date) ==
	floor((yyyymmddModifyAux(date) + calculationCoefficientOfDate - floor(daysInYear * yearAux(date))) / averageDaysInMonth);

yyyymmddModifyAux: Date -> real
yyyymmddModifyAux(date) == 
	let	julianDate = mjd2Jd(date.getModifiedJulianDate()),
		century =  floor((julianDate + centuryCalculationCoefficient) / 36524.25)
	in	
		if julianDate > theDayBeforeGregorioCalendarStarted then
			julianDate + centuryCalculationCoefficient + century - century div 4 + 0.5
		else
			julianDate + 32082.9 + 0.5;

yearAux: Date -> int
yearAux(date) == floor (yyyymmddModifyAux(date) / daysInYear);

public getVernalEquinoxOnGMT: int -> Date
getVernalEquinoxOnGMT(year) ==
	let	y = year / 1000.0	in
	modifiedJulianDate2Date(
		julianDate2ModifiedJulianDate(1721139.2855 + 365.2421376 * year + y * y *  (0.067919 - 0.0027879 * y)));
	
public getSummerSolsticeOnGMT: int -> Date
getSummerSolsticeOnGMT(year) ==
	let	y = year / 1000.0	in
	modifiedJulianDate2Date(
		julianDate2ModifiedJulianDate(1721233.2486 + 365.2417284 * year - y * y * (0.053018 - 0.009332 * y)));	
	 
public getAutumnalEquinoxOnGMT: int -> Date
getAutumnalEquinoxOnGMT(year) ==
	let	y = year / 1000.0	in
	modifiedJulianDate2Date(
		julianDate2ModifiedJulianDate (1721325.6978 + 365.2425055 * year - y * y * (0.126689 - 0.0019401 * y)));

public getWinterSolsticeOnGMT: int -> Date
getWinterSolsticeOnGMT(year) ==
	let	y = year / 1000.0	in
	modifiedJulianDate2Date(
		julianDate2ModifiedJulianDate(1721414.392 + 365.2428898 * year - y * y * (0.010965 - 0.0084855 * y)));


  public getVernalEquinox : int -> Date
 getVernalEquinox(year) == getDateInStandardTime(getVernalEquinoxOnGMT(year));
 
 public getSummerSolstice : int -> Date
 getSummerSolstice(year) == getDateInStandardTime(getSummerSolsticeOnGMT(year));
 
 public getAutumnalEquinox : int -> Date
 getAutumnalEquinox(year) == getDateInStandardTime(getAutumnalEquinoxOnGMT(year));
 
 -- Now, I can't get the right Winter Solstice in leap year
 public getWinterSolstice : int -> Date
 getWinterSolstice(year) == getDateInStandardTime(getWinterSolsticeOnGMT(year));


----calculation

public dateAdding: Date * int -> Date
dateAdding(date,addNumOfDays) == date.plus(addNumOfDays);

public diffOfDates: Date * Date -> int
diffOfDates(date1,date2) == floor(date1.getModifiedJulianDate() - date2.getModifiedJulianDate());

--dateからnumOfDaysを減算したdateを返す
public dateSubtracting: Date * int -> Date
dateSubtracting(date,subtractNumOfDays) == date.minus(subtractNumOfDays);

----Conversion

public mjd2Jd: real -> real
mjd2Jd(modifiedJulianDate) == modifiedJulianDate + daysDifferenceOfModifiedJulianDate;

public julianDate2ModifiedJulianDate: real -> real
julianDate2ModifiedJulianDate(julianDate) == julianDate - daysDifferenceOfModifiedJulianDate;

--yyyymmddを通常の値の範囲内に変換する。
--new Calendar().getRegularDate(2003, 14, 29) = getDateFrom_yyyy_mm_dd(2004, 2, 29)
public getRegularDate : int * int * int -> Date
getRegularDate(candidateYear, candidateOfMonth, candidateDate) ==
	let	mk_(year, month) = getRegularMonth(candidateYear, candidateOfMonth)
	in
	getDateFrom_yyyy_mm_dd(year, month, candidateDate);

--年月を通常の値の範囲内に変換する。
public getRegularMonth : int * int -> int * int
getRegularMonth(candidateYear, candidateOfMonth) ==
	let	year = 
			if candidateOfMonth <= 0 then
				candidateYear + (candidateOfMonth - 12) div monthsInYear
			else
				candidateYear + (candidateOfMonth - 1) div monthsInYear,
		candidateOfMonth2 = candidateOfMonth mod monthsInYear,
		month = 
			if candidateOfMonth2 = 0 then
				12
			else
				candidateOfMonth2
	in
	mk_(year, month);
	
	
--(整数三つ組の)date2Year(2001,7,1) = 2001.5
public date2Year:  int * int * int
	-> 
	real	--dateをYear(実数)に変換した値
date2Year(year, month, day) == year + (month - 1) / monthsInYear + (day - 1.0) / daysInYear;

public date2Str : Date +> seq of char
date2Str(date) == date.date2Str();

public convertDateFromString : seq of char +> [Date]
convertDateFromString(dateStr) == 
	let	date = getDateFromString(dateStr)
   	in	if date = false then nil
   		else date;

--以下は、休日の考慮をした機能で、サブクラスで休日の集合を定義する必要がある。

/* Query */
--2つのdateの間の休日の集合を返す。日曜日である休日も含むが、休日でない日曜日は含まない。
public getSetOfDayOffBetweenDates : Date * Date -> set of Date
getSetOfDayOffBetweenDates(date1,date2) ==
	let	Date1 = min(date1)(date2),
		Date2 = max(date1)(date2),
		setOfYear = {Year(Date1),...,Year(Date2)},
		setOfDayOff = dunion {getSetOfDayOff(year) | year in set setOfYear}
	in
	{dayOff | dayOff in set setOfDayOff & date1.LE(dayOff) and dayOff.LE(date2)};

--2つのdateの間の休日の数を返す。日曜日である休日も含むが、休日でない日dayOfWeekは含まない。
public getDayOffsExceptSunday: Date * Date -> int
getDayOffsExceptSunday(date1,date2) == card (getSetOfDayOffBetweenDates(date1,date2));

--2つのdateの間の休日あるいは日曜日の数を返す(startDateを含む)
public getTheNumberOfDayOff: Date * Date -> int
getTheNumberOfDayOff(date1,date2) ==
	let	Date1 = min(date1)(date2),
		Date2 = max(date1)(date2),
		numberOfSunday = getNumberOfTheDayOfWeek(Date1,Date2,<Sun>)	in
	numberOfSunday + card getSetOfNotSundayDayOff(Date1,Date2);

--2つのdateの間の休日あるいは日曜日の数を返す(startDateを含まない)
public getTheNumberOfDayOffExceptStartDate: Date * Date -> int
getTheNumberOfDayOffExceptStartDate(date1,date2) ==
	let	Date1 = min(date1)(date2),
		Date2 = max(date1)(date2)	in
	getTheNumberOfDayOff(Date1.plus( 1), Date2);

private getSetOfNotSundayDayOff : Date * Date -> set of Date
getSetOfNotSundayDayOff(date1,date2) ==
	let	setOfDayOff = getSetOfDayOffBetweenDates(date1,date2)	in
	{dayOff | dayOff in set setOfDayOff & not isSunday(dayOff)};

--日曜日である休日の集合を返す
public getDayOffsAndSunday : Date * Date -> set of Date
getDayOffsAndSunday(date1,date2) == 
	let	setOfDayOff = getSetOfDayOffBetweenDates(date1,date2)	in
	{dayOff | dayOff in set setOfDayOff & isSunday(dayOff)};

/* Conversion */

--休日でないdateを返す(未来へ向かって探索する)
public getFutureWeekday : Date-> Date
getFutureWeekday(date) ==
	cases  isSundayOrDayoff(date) or isSaturday(date):
		(true)	-> getFutureWeekday(date.plus( 1)),
		others	-> date
	end;

--休日でないdateを返す(過去へ向かって探索する)
public getPastWeekday : Date-> Date
getPastWeekday(date) ==
	cases   isSundayOrDayoff(date) or isSaturday(date):
		(true)	-> getPastWeekday (date.minus(1)),
		others	-> date
	end
	measure getPastWeekdaymeasure;

getPastWeekdaymeasure : Date +> nat
getPastWeekdaymeasure(d) == d.getModifiedJulianDate();

--与えられた平日に、平日n日分を加算する
public addWeekday : Date * int -> Date
addWeekday(date,addNumOfDays) == addWeekdayAux(getFutureWeekday(date),addNumOfDays);

public addWeekdayAux : Date * int -> Date
addWeekdayAux(date,addNumOfDays) ==
	cases isSundayOrDayoff(date) or isSaturday(date):
		(true)	-> addWeekdayAux(date.plus(1),addNumOfDays),
		others	->
					if addNumOfDays <= 0 then
						date
					else
						addWeekdayAux(date.plus(1), addNumOfDays-1)
	end;

--与えられた平日に、平日n日分を減算する
public subtractWeekday : Date * int -> Date
subtractWeekday(date,subtractNumOfDays) == subtractWeekdayAux(getPastWeekday(date),subtractNumOfDays);

public subtractWeekdayAux : Date * int -> Date
subtractWeekdayAux(date,subtractNumOfDays) ==
	cases isSundayOrDayoff(date) or isSaturday(date):
		(true)	-> subtractWeekdayAux(date.minus(1),subtractNumOfDays),
		others	->
					if subtractNumOfDays <= 0 then
						date
					else
						subtractWeekdayAux(date.minus(1), subtractNumOfDays-1)
	end;

/* Query */

public isDayOff : Date -> bool 
isDayOff(date) == 
	let	setOfDayOff = {d.getModifiedJulianDate() | d in set getSetOfDayOff(date.Year())}	in
	date.getModifiedJulianDate() in set setOfDayOff;
	
public isSundayOrDayoff : Date -> bool
isSundayOrDayoff(date) ==  isSunday(date) or isDayOff(date);

public isInDateSet :  Date * set of Date -> bool
isInDateSet(date, aNationalHolidaySet) == (
	let holidaySetByModifiedJulianDate = {floor d.getModifiedJulianDate() | d in set aNationalHolidaySet}
	in
	date.getModifiedJulianDate() in set holidaySetByModifiedJulianDate
  );

operations

public modifiedJulianDate2Date: real ==> Date
modifiedJulianDate2Date(modifiedJulianDate) == 
	return new Date(self,modifiedJulianDate);
	
public getDateFrom_yyyy_mm_dd: int * int * int  ==> Date
getDateFrom_yyyy_mm_dd(year, month, day) ==
	let	[y,m] = if (month > correctedMonths - monthsInYear) then
			[year + calculationCoefficientOfYear , month + 1]
		else
			[year + calculationCoefficientOfYear - 1 , month + correctedMonths - 1],
		century = y div yearInCentury,
	 	centuryCoefficient =		if (date2Year(year, month, day) > theFirstDayOfGregorioCalendar) then
						century div 4 - century - 32167.0
					else
						-32205.0,
		haldDay = 0.5	
	in
	return 
		modifiedJulianDate2Date(floor(daysInYear * y) + 
		floor(averageDaysInMonth * m) + day + centuryCoefficient - haldDay - daysDifferenceOfModifiedJulianDate);

public getDateFromString :
	seq of char	--yyyymmdd
	==>
	Date | bool	-- if not date then false
getDateFromString(yyyymmdd) ==
	(if not String`isDigits(yyyymmdd) then
		return false;
	let	yyyymmddByInt = String`asInteger(yyyymmdd),
		year = yyyymmddByInt div 10000,
		mmddByInt = yyyymmddByInt mod 10000,
		month =  mmddByInt div 100,
		day =  mmddByInt mod 100
	in
		if getDateFrom_yyyy_mm_dd(year,month,day).date2Str() = yyyymmdd then
			return getDateFrom_yyyy_mm_dd(year,month,day)
		else
			return false
	);

public getDateInStandardTime : Date ==> Date	
getDateInStandardTime(date) == 
	return modifiedJulianDate2Date (date.getModifiedJulianDate() + date.calendar().getDifferenceWithGMT());	

public getDayOfTheWeekInYear : int * NameOfDayOfTheWeek ==> set of Date
getDayOfTheWeekInYear(year,dayOfWeek) ==
	(
	dcl	aSetOfTheDayOfWeek : set of Date := {},
		date : Date := self.getNthDayOfTheWeek(year,1,1,dayOfWeek);
	while date.LE(self.lastDayOfTheWeekInMonth(year,12,dayOfWeek)) do (
		 aSetOfTheDayOfWeek :=  aSetOfTheDayOfWeek union {date};
		date := date.plus(7)
	);
	return aSetOfTheDayOfWeek
	);

public getDifferenceWithGMT : () ==> real
getDifferenceWithGMT() == return differenceWithGMT;

public setDifferenceWithGMT : (real) ==> ()
setDifferenceWithGMT(diff) == differenceWithGMT := diff;

public setTheSetOfDayOffs: int ==> ()
setTheSetOfDayOffs(-) == is subclass responsibility;
	
public getSetOfDayOff: int ==> set of Date 
getSetOfDayOff(aYear) == 
	(
	if not aYear in set dom Year2Holidays then
		self.setTheSetOfDayOffs(aYear);
	return self.Year2Holidays(aYear)
	);
	
--read todayfrom a file
public readToday : seq of char ==> [Date]
readToday(fname) ==
	let	mk_(r, mk_(y, m, d)) = io.freadval[int * int * int](fname)
	in
	if r then
		return getDateFrom_yyyy_mm_dd(y,m,d)
	else
		let	- = io.echo("Can't read today's data file.")
		in
		return nil;

--stub functions for getting today
public today: () ==> Date
today() == 
	if iToday = nil then
		return readToday(homedir ^ "/temp/Today.txt")	
	else
		return iToday;

--todayのdateを指定したreadFromFile。
public readFromFiletoday: seq of char ==> Date
readFromFiletoday(fname) == 
	if iToday = nil then
		return readToday(fname)	
	else
		return iToday;

public setToday : Date ==> ()
setToday(date) == iToday := date;
	
end Calendar

UseReal.vdmpp

class UseReal

instance variables
	r : Real := new Real()	

traces

S1: let n in set {0, 1, 9, 10, 99, 199, 0.1, 9.1, 10.1, 10.123} in r.numberOfDigit(n)

end UseReal

Term.vdmpp

class Term

values
	Rcsid = "$Id: Term.vpp,v 1.1 2005/10/31 02:15:42 vdmtools Exp $";

instance variables
startTime : [Time];
endTime : [Time];

functions
static public isInThePeriod : Time * Term -> bool
isInThePeriod(aTime, aPeriod) ==
	(aPeriod.getStartTime() = nil or aPeriod.getStartTime().LE(aTime)) and
	(aPeriod.getEndTime() = nil or aPeriod.getEndTime().GE(aTime));

public EQ : Term -> bool
EQ(aPeriod) == 
	self.getStartTime().EQ(aPeriod.getStartTime()) and self.getEndTime().EQ(aPeriod.getEndTime());

operations
public Term:[Time]*[Time] ==> Term
Term(astartTime, aendTime) ==
	(
	startTime := astartTime;
	endTime := aendTime;
	return self
	);

public getStartTime : () ==> [Time]
getStartTime() == return startTime;

public getEndTime : () ==> [Time]
getEndTime() == return endTime;
	
end  Term

Queue.vdmpp

class Queue

functions
static public empty[@T] : () -> seq of @T
empty() == [];

static public isEmpty[@T] : seq of @T -> bool
isEmpty(s) == s = [];
	
static public enQueue[@T] : @T * seq of @T -> seq of @T
enQueue(anElem, aQueue) == aQueue ^ [anElem];

static public deQueue[@T] : seq of @T -> seq of @T
deQueue(aQueue) == 
	if aQueue = [] then
		[]
	else
		tl aQueue;

static public top[@T] : seq of @T -> [@T]
top(aQueue) == 
	if aQueue = [] then
		nil
	else
		hd aQueue;

end Queue

UseUniqueNumber.vdmpp

class UseUniqueNumber

instance variables
sUN : UniqueNumber :=  new UniqueNumber()

traces

S1 : 
	let n in set {1,...,4} in sUN.getUniqNumStr(n){100}

end UseUniqueNumber

SBCalendar.vdmpp

                                                                                                                                                                          	
class SBCalendar is subclass of JapaneseCalendar -- date

values
	io = new IO();
	calendar = new SBCalendar();

instance variables

public iTodayOnBusiness : [Date] := nil;	-- This value express today for test.
public iTodayOnCompanyMap : [map seq of char to Date] := { |-> };		-- a map of companyCode to todayOnBusiness
public timeOfSystem : [Time] := nil;	-- This value express now for test.

functions

static public isCorrectContractMonth: seq of char -> bool
isCorrectContractMonth(aContractMonth) ==
	calendar.getDateFromString(aContractMonth ^ "01") <> false;

static public getExerciseDate :  seq of char -> Date
getExerciseDate(aContractMonth) ==
	let	firstDayOfContractMonth = calendar.getDateFromString(aContractMonth ^ "01"),
		designatedYear = firstDayOfContractMonth.Year(),
		designatedMonth =firstDayOfContractMonth.Month()	in
	calendar.getNthDayOfTheWeek(designatedYear,designatedMonth,2,<Fri>).getPastWeekday()
pre
	isCorrectContractMonth(aContractMonth);
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 	
static public getContractDate : Date -> Date 
getContractDate(aDate) == 	
	let	 
		mk_(year, month) = calendar.getMonthOf6monthsLater(aDate.Year(), aDate.Month()),
		date = aDate.day(),
		candidateDate = getCandidateDate(year, month, date)
	in
	candidateDate.getPastWeekday()	--Sometime the result is a date of previous month. 
--pre
	--aDate.isNotDayOff()
post	
	let	
		mk_(year, month) = calendar.getMonthOf6monthsLater(aDate.Year(), aDate.Month()),
		date = aDate.day(),
		candidateDate = getCandidateDate(year, month, date) 
	in
	RESULT.EQ(candidateDate.getPastWeekday()) and
	if isDayoffFromTheBeginingOfMonthToCandidateDate(candidateDate) then
		RESULT.Month() = getPreviousMonth(year, month) 
	else
		RESULT.Month() = month;

static public getMonthOf6monthsLater :  int * int ->  int * int
getMonthOf6monthsLater(year, month) == calendar.getRegularMonth(year, month+6);

static public getCandidateDate : int * int * int -> Date
getCandidateDate(year, month, date)  == 
		let	dateOfEndOfMonth = calendar.getLastDayOfMonth(year, month)
		in
			if dateOfEndOfMonth.day() < date then
				dateOfEndOfMonth
			else
				calendar.getDateFrom_yyyy_mm_dd(year, month, date);

static public isDayoffFromTheBeginingOfMonthToCandidateDate : Date -> bool
isDayoffFromTheBeginingOfMonthToCandidateDate(candidateDate) == 
	forall day in set {1, ..., candidateDate.day()} & 
		calendar.isSundayOrDayoff(calendar.getDateFrom_yyyy_mm_dd(candidateDate.Year(), candidateDate.Month(), day));

static public getPreviousMonth : int * int -> int
getPreviousMonth(year, month) == 
		let	mk_(-, previousMonth) = calendar.getRegularMonth(year, month-1)
		in
		previousMonth;

static public isDateNil: [Date] -> bool
isDateNil(date) ==  date = nil; --or date = maxDate();

static public systemDate : () -> Date
systemDate() == calendar.today();

operations
public setTheSetOfDayOffs: int ==> () 	-- get the set of dayoff, but Sundays are not in set
setTheSetOfDayOffs(year) ==
	let	japaneseCalendar = new JapaneseCalendar(),
		japaneseDayoffSet = japaneseCalendar.getSetOfDayOff(year),
		TR1のsetOfDayOff = {
			japaneseCalendar.getDateFrom_yyyy_mm_dd(year,1,2), 
			japaneseCalendar.getDateFrom_yyyy_mm_dd(year,1,3), 
			japaneseCalendar.getDateFrom_yyyy_mm_dd(year,12,29), 
			japaneseCalendar.getDateFrom_yyyy_mm_dd(year,12,30), 
			japaneseCalendar.getDateFrom_yyyy_mm_dd(year,12,31)
		},
		saturdaySet = japaneseCalendar.getDayOfTheWeekInYear(year,<Sat>) 	in
	Year2Holidays := Year2Holidays munion { year |-> japaneseDayoffSet union TR1のsetOfDayOff union saturdaySet}
pre
	year >= 2000;

--todayOnBusinessをreadFromFile
public readTodayOnBusiness : seq of char ==> [Date]
readTodayOnBusiness(fname) ==
	let	mk_(rslt, mk_(y,m,d)) = io.freadval[int * int * int](fname)
	in
	if rslt then
		return getDateFrom_yyyy_mm_dd(y,m,d)
	else
		let	- = io.echo("Can't read BaseDay's data file.")
		in
		return nil;

--get today for test
public todayOnBusiness: () ==> Date
todayOnBusiness() == 
	if iTodayOnBusiness = nil then
		return readTodayOnBusiness(homedir ^ "/temp/BaseDay.txt")
	else
		return iTodayOnBusiness;

public readFromFiletodayOnBusiness: seq of char ==> Date
readFromFiletodayOnBusiness(fname) == 
	if iTodayOnBusiness = nil then
		return readTodayOnBusiness(fname)
	else
		return iTodayOnBusiness;

public setTodayOnBusiness : Date ==> ()
setTodayOnBusiness(date) == iTodayOnBusiness := date;

-- get today for system. For example, many business systems thinks just after midnight is as "today"
public todayOnCompany: seq of char ==> Date
todayOnCompany(companyCode) == 
	(
	if iTodayOnCompanyMap = nil then
		setTodayOnCompany(companyCode,todayOnBusiness());
	return iTodayOnCompanyMap(companyCode)
	);

public setTodayOnCompany : seq of char * Date ==> ()
setTodayOnCompany(companyCode,date) == iTodayOnCompanyMap := iTodayOnCompanyMap ++ { companyCode |-> date };

public readSystemTime : () ==> [Time]
readSystemTime() ==
	let	mk_(rslt, now) = io.freadval[Time](homedir ^ "/temp/SystemTime.txt")
	in
	if rslt then
		return now
	else
		let	- = io.echo("Can't read System Time data file.")
		in
		return nil;

public systemTime : () ==> Time
systemTime() == 
	if timeOfSystem = nil then
		readSystemTime()
	else
		return timeOfSystem;

public setSystemTime : Time ==> ()
setSystemTime(t) ==  timeOfSystem := t;

public SBCalendar : () ==> SBCalendar
SBCalendar() ==
	(
	setDifferenceWithGMT(differenceBetweenGMTandJST); 
	return self
	);
	
end SBCalendar
                                                                          

Real.vdmpp

class Real

values
	Tolerance = 1e-8;
	Variation = 1e-5;	

functions

static public EQ : real -> real -> bool
EQ(r1)( r2) == abs(r1 - r2) < Tolerance;

static public EQE : real -> real -> real -> bool
EQE(e)(r1)(r2) == abs(r1 - r2) < e;

static public numberOfDigit : real -> nat
numberOfDigit(x) ==
	let	i = floor(x)	in
	if x = i then
		aNumberOfIntegerPartDigit(i)
	else
		aNumberOfIntegerPartDigit(i) + 1 + getNumberOfDigitsAfterTheDecimalPoint(x);

static public aNumberOfIntegerPartDigit : int -> nat
aNumberOfIntegerPartDigit(i) == aNumberOfIntegerPartDigitAux(i, 1);

static public aNumberOfIntegerPartDigitAux : int * nat -> nat
aNumberOfIntegerPartDigitAux(i, numberOfDigit) ==
	let	q = i div 10 in
	cases q:
		0		-> numberOfDigit,
		others	-> Real`aNumberOfIntegerPartDigitAux(q, numberOfDigit + 1)
	end
measure idiv10;

static idiv10 : int * nat +> nat
idiv10(i, -) == i div 10;

static public isNDigitsAfterTheDecimalPoint : real * nat -> bool
isNDigitsAfterTheDecimalPoint(x,numberOfDigit) == 
	getNumberOfDigitsAfterTheDecimalPoint(x) = numberOfDigit;

static public getNumberOfDigitsAfterTheDecimalPoint : real -> nat
getNumberOfDigitsAfterTheDecimalPoint(x) == getNumberOfDigitsAfterTheDecimalPointAux(x,0);

static getNumberOfDigitsAfterTheDecimalPointAux : real * nat -> nat
getNumberOfDigitsAfterTheDecimalPointAux(x,numberOfDigit) ==
	if x = floor(x) then
		numberOfDigit
	else
		getNumberOfDigitsAfterTheDecimalPointAux(x * 10, numberOfDigit + 1);

static public roundAterDecimalPointByNdigit : real * nat -> real
roundAterDecimalPointByNdigit(r, numberOfDigit) ==
	let	multiple = 10 ** numberOfDigit
	in
	floor(r * multiple  + 0.5) / multiple
pre
	r >= 0;

static public Differentiate : (real -> real) ->real -> real
Differentiate(f)(x) == (f(x+Variation) - f(x)) / Variation ;

--Newton's method to solve the equation
static public NewtonMethod: (real ->real) -> real -> real
NewtonMethod(f)(x) ==
	let	terminationCondition = lambda y : real &  abs(f(y)) < Tolerance,
		nextApproximation = lambda y : real & y - (f(y) / Differentiate(f)(y))	in
	new Function().Funtil[real](terminationCondition)(nextApproximation)(x);
	
-- Integration by Trapezoidal rule algorithm. This is too bad :-)
static public integrate : (real -> real)  -> nat1 -> real -> real -> real
integrate(f)(n)(a)(b) == 
	let	
		h = (b - a) / n,
		s = seqGenerate(n, a, h)
	in
	h * (f(a) / 2 + Sequence`Sum[real](Sequence`fmap[real, real](f)(s)) + f(b) / 2);

operations
static private seqGenerate : nat1 * real * real  ==> seq of real
seqGenerate(n, a, h) == 
	(	
		dcl s : seq of real := [];
		for i = 1 to n do
		s := s ^ [a + i * h];
	return s
	);

functions
--get root value for testing Newton Method.
static public root: real -> real
root(x) ==
	let	f = lambda y : real & y ** 2 - x	in
	NewtonMethod(f)(x);

static public getTotalPrincipal : real * int -> real
getTotalPrincipal(Interest,year) == (1 + Interest) ** year
pre
	Interest >= 0 and year > 0;

static getInterestImplicitSpec_Math_version : real * int -> real
getInterestImplicitSpec_Math_version(multiple,year) == is not yet specified
pre
	multiple > 1.0 and year > 0 
post
	multiple > 1.0 and year > 0 and
	exists1 Interest : real &
		let totalPrincipalAndInterest = getTotalPrincipal(Interest,year)
		in multiple = totalPrincipalAndInterest  and RESULT = Interest;
		
static getInterestImplicitSpec_Computer_version : real * int -> real
getInterestImplicitSpec_Computer_version(multiple,years) ==
	is not yet specified
pre
	multiple > 1.0 and years > 0 
post
	multiple > 1.0 and years > 0 and
	exists1 Interest : real & 
		let	totalPrincipalAndInterest = getTotalPrincipal(Interest,years)
		in	EQ(multiple)(totalPrincipalAndInterest) and RESULT = Interest;

--getInterest explicit specification
static public getInterest: real * int -> real
getInterest(multiple,years) ==
	let	f = lambda Interest : real & multiple - getTotalPrincipal(Interest,years)	in
	NewtonMethod(f)(0);
	
end Real

TimeT.vdmpp

class TimeT is subclass of TestDriver 
functions
public tests : () -> seq of TestCase
tests() == 
	[ 
	new TimeT06(), new TimeT05(), new TimeT04(),
	new TimeT03(), new TimeT02(), new TimeT01()
	];
end TimeT
----------------------------------------------------------

class TimeT01 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	cal = new JapaneseCalendar(),
		d1 = cal.getDateFrom_yyyy_mm_dd(2003, 7, 30),
		d3 = cal.getDateFrom_yyyy_mm_dd(2003, 8, 15),
		t1 = new Time(cal, 2003, 7, 30, 14, 29, 30, 20),
		t2 = new Time(cal, 2003, 8, 1) ,
		t3 = new Time(d3)
	in
	return
		t1.getDate().EQ(d1) and 
		t1.Time2IntProduct(t1.getTime()) = mk_(14, 29, 30, 20) and 
		mk_(t1.hour(), t1.minute(), t1.second()) = mk_(14, 29, 30) and
		mk_(t2.Year(), t2.Month(), t2.day()) = mk_(2003, 8, 1) and 
		t2.getTime() = t2.IntProduct2TimeMillieSeconds(0, 0, 0, 0) and
		t3.getDate().EQ(d3) and 
		t3.getTime() = t2.IntProduct2TimeMillieSeconds(0, 0, 0, 0) 
	;
protected setUp: () ==> ()
setUp() == TestName := "Time01:¥tTest of constructor.";
protected tearDown: () ==> ()
tearDown() == return;
end TimeT01
----------------------------------------------------------

class TimeT02 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	cal = new JapaneseCalendar(),
		t1 = new Time(cal, 2003, 7, 30, 14, 29, 30, 0),
		t2 = new Time(cal, 2003, 8, 1) ,
		t4 = new Time(cal, 2003, 7, 30, 14, 29, 31, 0),
		t5 = new Time(cal, 2003, 7, 30, 14, 29, 31, 0),
		t6 = t1
	in
	return 
		t1.LT(t2) and
		t1.LT(t4) and
		t1.LE(t2) and
		t1.LE(t4) and
		t2.GT(t1) and
		t4.GT(t1) and
		t2.GE(t1) and
		t4.GE(t1) and
		t4.EQ(t5) and
		t4.NE(t1) and
		t4 <> t5 and
		t1 = t6
	;
protected setUp: () ==> ()
setUp() == TestName := "TimeT02:\tATime comparing.";
protected tearDown: () ==> ()
tearDown() == return;
end TimeT02
----------------------------------------------------------

class TimeT03 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	cal = new JapaneseCalendar(),
		t = new Time(cal, 2003, 7, 30, 14, 29, 30, 0),
		t1 = t.plussecond(20),
		t2 = t.plussecond(30),
		t3 = t.plussecond(50),
		t4 = t.plussecond(90),
		t5 = t.plussecond(150),
		t6 = t.plussecond(3600),
		t7 = t.plusminute(30),
		t8 = t.plusminute(31),
		t9 = t.plusminute(40),
		t10 = t.plusminute(91),
		t11 = t.plusminute(1440),
		t12 = t.plus(9, 30, 30, 123),
		t13 = t.plushour(48),
		t14 = t.plus(0, 0, 0, 0)
	in
	return 
		t1.minute() = 29 and t1.second() = 50 and
		t2.minute() = 30 and t2.second() = 0 and
		t3.minute() = 30 and t3.second() = 20 and
		t4.minute() = 31 and t4.second() = 0 and
		t5.hour() = 14 and t5.minute() = 32 and t5.second() = 0 and  
		t6.hour() = 15 and t6.minute() = 29 and t6.second() = 30 and  
		t7.hour() = 14 and t7.minute() = 59 and
		t8.hour() = 15 and t8.minute() = 0 and
		t9.hour() = 15 and t9.minute() = 9 and
		t10.hour() = 16 and t10.minute() = 0 and t10.second() = 30 and
		t11.Year() = 2003 and t11.Month() = 7 and t11.day() = 31 and t11.hour() = 14 and t11.minute() = 29 and t11.second() = 30 and
		t12.Year() = 2003 and t12.Month() = 7 and t12.day() = 31 and t12.hour() = 0 and t12.minute() = 0 and t12.second() = 0 and t12.milliSecond() = 123 and
		t13.Year() = 2003 and t13.Month() = 8 and t13.day() = 1 and t13.hour() = 14 and t13.minute() = 29 and t13.second() = 30 and t13.milliSecond() = 0 and
		t13.asString() = "20030801142930000" and
		t13.print() = "Year=2003, Month=08, Day=01, 14Hour, 29Minute, 30Second, 000MilliSecond" and
		t14.asString() = "20030730142930000"
	;
protected setUp: () ==> ()
setUp() == TestName := "TimeT03:\tTime ading.";
protected tearDown: () ==> ()
tearDown() == return;
end TimeT03
----------------------------------------------------------

class TimeT04 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	cal = new JapaneseCalendar(),
		t = new Time(cal, 2003, 7, 30, 14, 29, 30, 0),
		t1 = t.minus(14, 30, 30, 0) ,
		t2 = t.minus(38, 30, 30, 0) ,
		t3 = t.plus(-38, -30, -30, 0),
		t4 = t.plus(-0, -0, -0, -0)
	in
	return 
		t1.Time2IntProduct(t1.getTime())  = mk_(23,59,0,0) and
		t1.getDate().date2Str() = "20030729" and
		t2.Time2IntProduct(t2.getTime())  = mk_(23,59,0,0) and
		t2.getDate().date2Str() = "20030728" and
		t3.Time2IntProduct(t3.getTime())  = mk_(23,59,0,0) and
		t3.getDate().date2Str() = "20030728" and
		t4.print() = "Year=2003, Month=07, Day=30, 14Hour, 29Minute, 30Second, 000MilliSecond"
		
	;
protected setUp: () ==> ()
setUp() == TestName := "TimeT04:\tATime subtracting.";
protected tearDown: () ==> ()
tearDown() == return;
end TimeT04
----------------------------------------------------------

class TimeT05 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	cal = new JapaneseCalendar(),
		t1 = new Time(cal, 2003, 7, 30, 14, 29, 30, 0),
		t2 = new Time(cal, 2003, 7, 30, 14, 29, 30, 0),
		t3 = new Time(cal, 2003, 7, 30, 14, 29, 30, 0),
		t4 = new Time(cal, 2003, 7, 30, 14, 29, 30, 0)
	in
	(
	t1.setTimeFromNat(15);
	t2.setMinuteFromNat(19);
	t3.setSecond(47);
	t4.setMilliSecond(789);
	return 
		t1.Time2IntProduct(t1.getTime())  = mk_(15, 29, 30, 0) and
		t2.Time2IntProduct(t2.getTime())  = mk_(14, 19, 30, 0) and
		t3.Time2IntProduct(t3.getTime())  = mk_(14, 29, 47, 0) and
		t4.Time2IntProduct(t4.getTime())  = mk_(14, 29, 30, 789) and
		t4.getDate().date2Str() = "20030730" 
	)	
	;
protected setUp: () ==> ()
setUp() == TestName := "TimeT05:\tSet instance variables.";
protected tearDown: () ==> ()
tearDown() == return;
end TimeT05
----------------------------------------------------------

class TimeT06 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	cal = new SBCalendar()
	in
	(
	return 
		new Time(cal).EQ(new Time(cal, 2001, 3, 1, 10, 11, 23, 456)) and
		new Time(homedir ^ "/temp/BaseDay.txt", homedir ^ "/temp/Now2.txt", cal).EQ(new Time(cal, 2003, 10, 24, 12, 34, 56, 789))
	)	
	;
protected setUp: () ==> ()
setUp() == TestName := "TimeT06:\tTest currentDateTime from file.";
protected tearDown: () ==> ()
tearDown() == return;
end TimeT06

NumberT.vdmpp

class NumberT is subclass of TestDriver 

functions
public tests : () -> seq of TestCase
tests () == 
	[ new NumberT01(),  new NumberT02(),  new NumberT03()
	];
end NumberT

class NumberT01 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	return
		(Number`min[int](lambda x:int, y:int & x < y)(-3)(4) = -3 and
		Number`min[int](lambda x:int, y:int & x < y)(4)(-3) = -3 and
		Number`min[nat](lambda x:nat, y:nat & x < y)(2)(10) = 2 and
		Number`min[int](lambda x:int, y:int & x < y)(0)(0) = 0 and
		Number`max[real](lambda x:real, y:real & x < y)(0.001)( -0.001) = 0.001 and
		Number`max[real](lambda x:real, y:real & x < y)(-0.001)( 0.001) = 0.001 and
		Number`max[real](lambda x:real, y:real & x < y)(0.0)(0.0) = 0.0)
;
protected setUp: () ==> ()
setUp() == TestName := "NumberT01:\tSummary of integer.";
protected tearDown: () ==> ()
tearDown() == return;
end NumberT01

class NumberT02 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	return
		 Number`isComputable[char]('a') = false and
		 Number`isComputable[int](-9) = true and
		 Number`isComputable[nat](0) = true and
		 Number`isComputable[nat1](1) = true and
		 Number`isComputable[real](1.234) = true and
		 Number`isComputable[rat](1.234) = true
;
protected setUp: () ==> ()
setUp() == TestName := "NumberT02:\tIs computable?";
protected tearDown: () ==> ()
tearDown() == return;
end NumberT02

class NumberT03 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	return
		 Number`min[seq of int](lambda s1: seq of int, s2 : seq of int & len s1 < len s2)([1,2])([1,2,3])  = [1, 2]  and
		 Number`max[seq of int](lambda s1: seq of int, s2 : seq of int & len s1 < len s2)([1,2])([1,2,3])  = [1, 2, 3] 
;
protected setUp: () ==> ()
setUp() == TestName := "NumberT03:\tType is not computable, but...";
protected tearDown: () ==> ()
tearDown() == return;
end NumberT03

FHashtableT.vdmpp

                                                         
class FHashtableT

functions
static public run : () +> bool
run() == 
let	testcases = [ t1(), t2(), t3(), t4(), t5(), t6() ]
in
FTestDriver`run(testcases);
                                                                  
static t1 : () -> FTestDriver`TestCase
t1() ==
	
	mk_FTestDriver`TestCase(
	"FHashtableT01:\t Test Contains, PutAll",
	let	aHashCode = lambda x : int & x mod 13,
		p1 = FHashtable`PutAll[int, seq of char]({ |-> })(aHashCode)(
				{1 |-> "Sahara", 2 |-> "Sato", 14 |-> "Sakoh"}
			),
		c1 = FHashtable`Contains[int, seq of char](p1)
	in
	c1("Sahara") and
	c1("Sato") and
	c1("Sakoh") and
	c1("") = false)
	;
                                                                            
static t2 : () -> FTestDriver`TestCase
t2() ==
	
	mk_FTestDriver`TestCase(
	"FHashtableT02:\t Test Clear, Remove, ContainsKey",
	let	aHashCode = lambda x : seq of char & if x = "" then "" else FSequence`Take[char](1)(x),
		h2 = FHashtable`PutAll[seq of char, int]({ |-> })(aHashCode)(
				{"a" |-> 1, "b" |-> 2, "c" |-> 3}
			),
		h3 = FHashtable`Clear[int, seq of char](),
		deletedh2 = FHashtable`Remove[seq of char, int](h2)(aHashCode)("b"),
		c1 = FHashtable`Contains[seq of char, int](deletedh2),
		ck1 = FHashtable`ContainsKey[seq of char, int](deletedh2)
	in
	h3 = {|->} and
	FHashtable`Get[seq of char, int](deletedh2)(aHashCode)("b") = nil and
	c1(2) = false and
	c1(1) and
	c1(3) and
	ck1("b") = false and 
	ck1("a") and
	ck1("c"))
	;
                                                          
static t3 : () -> FTestDriver`TestCase
t3() ==
	
	mk_FTestDriver`TestCase(
	"FHashtableT03:\t Test Put, Get",
	let	aHashCode = lambda x : int & x mod 13,
		put = FHashtable`Put[int, seq of char],
		p1 = put({ |-> })(aHashCode)(1)("Sahara"),
		p2 = put(p1)(aHashCode)(2)("Bush"),
		p3 = put(p2)(aHashCode)(2)("Sato"),
		p4 = put(p3)(aHashCode)(14)("Sakoh"),
		get = FHashtable`Get[int, seq of char](p4),
		g = FHashtable`Get[int, seq of char](p4)(aHashCode)
	in
	get(aHashCode)(1) = "Sahara" and
	get(aHashCode)(2) = "Sato" and
	get(aHashCode)(14) = "Sakoh" and
	get(aHashCode)(99) = nil and
	FSequence`Fmap[int, seq of char](g)([1, 14]) = ["Sahara", "Sakoh"] and
	FSequence`Fmap[int, seq of char](g)([1, 2]) = ["Sahara", "Sato"] 
	)
	;
                                                                  
static t4 : () -> FTestDriver`TestCase
t4() ==
	
	mk_FTestDriver`TestCase(
	"FHashtableT04:\t Test KeySet, ValueSet",
	let	aHashCode = lambda x : int & x mod 13,
		put = FHashtable`Put[int, seq of char],
		p1 = put({ |-> })(aHashCode)(1)("Sahara"),
		p2 = put(p1)(aHashCode)(2)("Bush"),
		p3 = put(p2)(aHashCode)(2)("Sato"),
		p4 = put(p3)(aHashCode)(14)("Sakoh"),
		k = FHashtable`KeySet[int, seq of char],
		v = FHashtable`ValueSet[int, seq of char]
	in
	k(p1) = {1} and
	v(p1) = {"Sahara"} and
	k(p2) = {1, 2} and
	v(p2) = {"Sahara", "Bush"} and
	k(p4) = {1,2,14} and
	v(p4) = {"Sahara", "Sato", "Sakoh"})
	;
                                                                            
static t5 : () -> FTestDriver`TestCase
t5() ==
	
	mk_FTestDriver`TestCase(
	"FHashtableT05:\t Test hashCode is duplicate",
	let	aHashCode1 = lambda x : int & x mod 13,
		h1 = FHashtable`PutAll[int, seq of char]({ |-> })(aHashCode1)(
				{1 |-> "SaharaShin", 2 |-> "SatoKei", 14 |-> "SakohHiroshi", 27 |-> "NishikawaNoriko"}
			),
		h2 = FHashtable`Remove[int, seq of char](h1)(aHashCode1)(14)
	in
	FHashtable`KeySet[int, seq of char](h2) = {1, 2, 27} and
	FHashtable`ValueSet[int, seq of char](h2) = {"SaharaShin",  "SatoKei", "NishikawaNoriko"})
	;
                                                      
static t6 : () -> FTestDriver`TestCase
t6() ==
	
	mk_FTestDriver`TestCase(
	"FHashtableT06:\t Test Size",
	let	aHashCode1 = lambda x : int & x mod 13,
		remove = FHashtable`Remove[int, seq of char],
		h1 = FHashtable`PutAll[int, seq of char]({ |-> })(aHashCode1)(
				{1 |-> "SaharaShin", 2 |-> "SatoKei", 14 |-> "SakohHiroshi"}
			),
		h2 = remove(h1)(aHashCode1)(1),
		h3 = remove(h2)(aHashCode1)(2),
		h4 = remove(h3)(aHashCode1)(14),
		isempty = FHashtable`IsEmpty[int, seq of char],
		size = FHashtable`Size[int, seq of char]
	in
	isempty(h4) and
	size(h4) = 0 and
	isempty(h3)  = false and
	size(h3) = 1 and
	size(h2) = 2 and
	size(h1) = 3)
	;

end FHashtableT
            

UniqueNumber.vdmpp

class UniqueNumber is subclass of CommonDefinition

values
DefaultValue = 1;

instance variables
protected UniqNum  : int := DefaultValue		-- UniqNum of next issued

functions
public getUniqNum : int * nat1 -> int
getUniqNum(aCandidateNum, aNumberOfDigit) == 
	if aCandidateNum >= 10 ** aNumberOfDigit then 
		initialize() 
	else
		aCandidateNum;

operations
-- make an unique number within aNumberOfDigit
public getUniqNumStr : nat1 ==> seq of char
getUniqNumStr(aNumberOfDigit) ==
	let	n = getUniqNum(UniqNum, aNumberOfDigit)
	in
	(
	UniqNum := UniqNum + 1;
	return Integer`asString(n)
	);
	
public initialize : () ==> int
initialize() == 
	(
	UniqNum := DefaultValue;
	return UniqNum
	);

end  UniqueNumber

SBCalendarT.vdmpp

class SBCalendarT is subclass of TestDriver
functions
public tests : () -> seq of TestCase
tests () == 
	[
	new SBCalendarT06(),
	new SBCalendarT05(),
	new SBCalendarT04(),
	new SBCalendarT03(),
	new SBCalendarT02(),
	new SBCalendarT01()
	];
end SBCalendarT

class SBCalendarT01 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	c = new SBCalendar()	in
	(
	c.setTodayOnBusiness(c.getDateFrom_yyyy_mm_dd(2001,9,12));
	c.setSystemTime(new Time(c, 2003, 10, 23, 13, 12, 34, 567));
	return
		(
		--c.maxDate().EQ(c.getDateFrom_yyyy_mm_dd(9999,12,31)) and
		--c.maxDate().date2Str = c.dateの最大値 and
		c.todayOnBusiness().EQ(c.getDateFrom_yyyy_mm_dd(2001,9,12)) and
		c.isDateNil(nil) = true and
		--c.isDateNil(c.maxDate()) = true and
		c.isDateNil(c.todayOnBusiness()) = false and
		c.systemDate().EQ(c.today()) and
		c.systemTime().EQ(new Time(c, 2003, 10, 23, 13, 12, 34, 567))
		)
	)
;
protected setUp: () ==> ()
setUp() == TestName := "SBCalendarT01:\tTest maxDate and date is nil.";
protected tearDown: () ==> ()
tearDown() == return;
end SBCalendarT01

class SBCalendarT02 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	jc = new SBCalendar(),
		setOfDayOff = jc.getSetOfDayOff(2001),
		setOfDayOff2006 = jc.getSetOfDayOff(2006),
		d0401 = jc.getDateFromString("20010401"),
		d0408 = jc.getDateFromString("20010408"),
		d0430 = jc.getDateFromString("20010430"),
		setOfDayOffBy_yyyy_mm_dd =  {jc.getYyyymmdd(dayOff) | dayOff in set setOfDayOff}	,
		setOfDayOffBy_yyyy_mm_dd2006 =  {jc.getYyyymmdd(dayOff) | dayOff in set setOfDayOff2006}	in
	return
		setOfDayOffBy_yyyy_mm_dd = 
			{ mk_( 2001,1,1 ),
			  mk_( 2001,1,2 ),
			  mk_( 2001,1,3 ),
			  mk_( 2001,1,6 ),
			  mk_( 2001,1,8 ),
			  mk_( 2001,1,13 ),
			  mk_( 2001,1,20 ),
			  mk_( 2001,1,27 ),
			  mk_( 2001,2,3 ),
			  mk_( 2001,2,10 ),
			  mk_( 2001,2,11 ),
			  mk_( 2001,2,12 ),
			  mk_( 2001,2,17 ),
			  mk_( 2001,2,24 ),
			  mk_( 2001,3,3 ),
			  mk_( 2001,3,10 ),
			  mk_( 2001,3,17 ),
			  mk_( 2001,3,20 ),
			  mk_( 2001,3,24 ),
			  mk_( 2001,3,31 ),
			  mk_( 2001,4,7 ),
			  mk_( 2001,4,14 ),
			  mk_( 2001,4,21 ),
			  mk_( 2001,4,28 ),
			  mk_( 2001,4,29 ),
			  mk_( 2001,4,30 ),
			  mk_( 2001,5,3 ),
			  mk_( 2001,5,4 ),
			  mk_( 2001,5,5 ),
			  mk_( 2001,5,12 ),
			  mk_( 2001,5,19 ),
			  mk_( 2001,5,26 ),
			  mk_( 2001,6,2 ),
			  mk_( 2001,6,9 ),
			  mk_( 2001,6,16 ),
			  mk_( 2001,6,23 ),
			  mk_( 2001,6,30 ),
			  mk_( 2001,7,7 ),
			  mk_( 2001,7,14 ),
			  mk_( 2001,7,20 ),
			  mk_( 2001,7,21 ),
			  mk_( 2001,7,28 ),
			  mk_( 2001,8,4 ),
			  mk_( 2001,8,11 ),
			  mk_( 2001,8,18 ),
			  mk_( 2001,8,25 ),
			  mk_( 2001,9,1 ),
			  mk_( 2001,9,8 ),
			  mk_( 2001,9,15 ),
			  mk_( 2001,9,22 ),
			  mk_( 2001,9,23 ),
			  mk_( 2001,9,24 ),
			  mk_( 2001,9,29 ),
			  mk_( 2001,10,6 ),
			  mk_( 2001,10,8 ),
			  mk_( 2001,10,13 ),
			  mk_( 2001,10,20 ),
			  mk_( 2001,10,27 ),
			  mk_( 2001,11,3 ),
			  mk_( 2001,11,10 ),
			  mk_( 2001,11,17 ),
			  mk_( 2001,11,23 ),
			  mk_( 2001,11,24 ),
			  mk_( 2001,12,1 ),
			  mk_( 2001,12,8 ),
			  mk_( 2001,12,15 ),
			  mk_( 2001,12,22 ),
			  mk_( 2001,12,23 ),
			  mk_( 2001,12,24 ),
			  mk_( 2001,12,29 ),
			  mk_( 2001,12,30 ),
			 mk_( 2001,12,31 ) } and
  		setOfDayOffBy_yyyy_mm_dd2006 =
			{ mk_( 2006,1,1 ),
			  mk_( 2006,1,2 ),
			  mk_( 2006,1,3 ),
			  mk_( 2006,1,7 ),
			  mk_( 2006,1,9 ),
			  mk_( 2006,1,14 ),
			  mk_( 2006,1,21 ),
			  mk_( 2006,1,28 ),
			  mk_( 2006,2,4 ),
			  mk_( 2006,2,11 ),
			  mk_( 2006,2,18 ),
			  mk_( 2006,2,25 ),
			  mk_( 2006,3,4 ),
			  mk_( 2006,3,11 ),
			  mk_( 2006,3,18 ),
			  mk_( 2006,3,21 ),
			  mk_( 2006,3,25 ),
			  mk_( 2006,4,1 ),
			  mk_( 2006,4,8 ),
			  mk_( 2006,4,15 ),
			  mk_( 2006,4,22 ),
			  mk_( 2006,4,29 ),
			  mk_( 2006,5,3 ),
			  mk_( 2006,5,4 ),
			  mk_( 2006,5,5 ),
			  mk_( 2006,5,6 ),
			  mk_( 2006,5,13 ),
			  mk_( 2006,5,20 ),
			  mk_( 2006,5,27 ),
			  mk_( 2006,6,3 ),
			  mk_( 2006,6,10 ),
			  mk_( 2006,6,17 ),
			  mk_( 2006,6,24 ),
			  mk_( 2006,7,1 ),
			  mk_( 2006,7,8 ),
			  mk_( 2006,7,15 ),
			  mk_( 2006,7,17 ),
			  mk_( 2006,7,22 ),
			  mk_( 2006,7,29 ),
			  mk_( 2006,8,5 ),
			  mk_( 2006,8,12 ),
			  mk_( 2006,8,19 ),
			  mk_( 2006,8,26 ),
			  mk_( 2006,9,2 ),
			  mk_( 2006,9,9 ),
			  mk_( 2006,9,16 ),
			  mk_( 2006,9,18 ),
			  mk_( 2006,9,23 ),
			  mk_( 2006,9,30 ),
			  mk_( 2006,10,7 ),
			  mk_( 2006,10,9 ),
			  mk_( 2006,10,14 ),
			  mk_( 2006,10,21 ),
			  mk_( 2006,10,28 ),
			  mk_( 2006,11,3 ),
			  mk_( 2006,11,4 ),
			  mk_( 2006,11,11 ),
			  mk_( 2006,11,18 ),
			  mk_( 2006,11,23 ),
			  mk_( 2006,11,25 ),
			  mk_( 2006,12,2 ),
			  mk_( 2006,12,9 ),
			  mk_( 2006,12,16 ),
			  mk_( 2006,12,23 ),
			  mk_( 2006,12,29 ),
			  mk_( 2006,12,30 ),
			  mk_( 2006,12,31 ) } and
  		jc.getDayOffsExceptSunday(d0401,d0430)  = 6 and
  		card jc.getDayOffsAndSunday(d0401,d0430) = 1 and
  		jc.getDayOffsAndSunday(d0401,d0408) = {}
	;
protected setUp: () ==> ()
setUp() == TestName := "SBCalendarT02:\tGetting set of day off.";
protected tearDown: () ==> ()
tearDown() == return;
end SBCalendarT02

class SBCalendarT03 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	c = new SBCalendar()	in
	(
	c.setTodayOnBusiness(c.getDateFrom_yyyy_mm_dd(2001,9,12));
	return
		(
		c.getExerciseDate("200111").EQ(c.getDateFrom_yyyy_mm_dd(2001,11,9))  and
		c.getExerciseDate("200109").EQ(c.getDateFrom_yyyy_mm_dd(2001,9,14))  and
		c.isCorrectContractMonth("200206") = true and
		c.isCorrectContractMonth("200206.01") = false and
		c.isCorrectContractMonth("Shin Sahara") = false 
		)
	)
;
protected setUp: () ==> ()
setUp() == TestName := "SBCalendarT03:\tTest validity checking of contract month and getting execution date.";
protected tearDown: () ==> ()
tearDown() == return;
end SBCalendarT03

class SBCalendarT04 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	c = new SBCalendar(),
		d0929 = c.getDateFrom_yyyy_mm_dd(2001, 9, 29),
		d0104 = c.getDateFrom_yyyy_mm_dd(20021, 1, 4)	in
	(
	c.setTodayOnCompany("007",d0104);
	c.setTodayOnCompany("009",d0929);
	return
		(
		c.todayOnCompany("007") = d0104 and
		c.todayOnCompany("009") = d0929 
		)
	)
;
protected setUp: () ==> ()
setUp() == TestName := "SBCalendarT04:\tTest of todayOnCompany";
protected tearDown: () ==> ()
tearDown() == return;
end SBCalendarT04

class SBCalendarT05 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	c = new SBCalendar()
	in
	return
		c.todayOnBusiness().EQ(c.getDateFrom_yyyy_mm_dd(2003, 10, 24)) and
		c.readFromFiletodayOnBusiness(homedir ^ "/temp/Today.txt").EQ(c.getDateFrom_yyyy_mm_dd(2001, 3, 1))
;
protected setUp: () ==> ()
setUp() == TestName := "SBCalendarT05:\tTest todayOnBusiness from a file.";
protected tearDown: () ==> ()
tearDown() == return;
end SBCalendarT05

class SBCalendarT06 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	c = new SBCalendar(),
		sDate = SBCalendar`getContractDate
	in
	return
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 1, 5)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 7, 5)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 1, 31)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 7, 30)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 2, 1)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 7, 30)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 2, 2)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 8, 2)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 2, 27)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 8, 27)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 3, 1)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 9, 1)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 3, 30)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 9, 30)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 3, 31)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 9, 30)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 4, 1)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 10, 1)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 4, 30)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 10, 29)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 5, 6)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 11, 5)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 5, 7)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 11, 5)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 5, 10)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 11, 10)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 6, 1)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 12, 1)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 6, 28)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 12, 28)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 6, 29)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 12, 28)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 6, 30)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 12, 28)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 7, 1)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 12, 28)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 7, 2)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 12, 28)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 7, 5)).EQ(c.getDateFrom_yyyy_mm_dd(2005, 1, 5)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2004, 7, 30)).EQ(c.getDateFrom_yyyy_mm_dd(2005, 1, 28)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2003, 8, 2)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 2, 2)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2003, 8, 28)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 2, 27)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2003, 8, 29)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 2, 27)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2003, 9, 1)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 3, 1)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2003, 9, 30)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 3, 30)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2003, 10, 1)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 4, 1)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2003, 10, 29)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 4, 28))  and
		sDate(c.getDateFrom_yyyy_mm_dd(2003, 11, 1)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 4, 30)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2003, 11, 30)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 5, 28)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2003, 12, 1)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 6, 1)) and
		sDate(c.getDateFrom_yyyy_mm_dd(2003, 12, 26)).EQ(c.getDateFrom_yyyy_mm_dd(2004, 6, 25))
;
protected setUp: () ==> ()
setUp() == TestName := "SBCalendarT06:\tGetting contract date of margin trading.";
protected tearDown: () ==> ()
tearDown() == return;
end SBCalendarT06

Sequence.vdmpp

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           	
class Sequence
	
functions 

static public Sum[@T]: seq of @T ->  @T
Sum(s) == SumAux[@T](s)(0)
pre
	is_(s, seq of real);

static SumAux[@T] : seq of @T -> @T -> @T
SumAux(s)(sum) ==
  if is_(s,seq of real) and is_real(sum)
  then
	if s = [] then
		sum
	else
		SumAux[@T](tl s)(sum + hd s)
  else undefined;
--measure length_measure;

static length_measure[@T] : seq of @T +> nat
length_measure(s) == len s;

static public Product[@T]: seq of @T ->  @T
Product(s) == ProductAux[@T](s)(1)
pre
	is_(s, seq of real);
 	
static ProductAux[@T] : seq of @T -> @T -> @T
ProductAux(s)(p) ==
 if is_(s,seq of real) and is_real(p)
 then
	cases s :
	[h] ^ tail	-> ProductAux[@T](tail)(p * h),
	[]			-> p
	end
 else undefined;
--measure length_measure;

static public GetAverage[@T]: seq of @T ->  [real]
GetAverage(s) == if s = [] then nil else GetAverageAux[@T](s)(0)(len s);

static GetAverageAux[@T] : seq of @T -> @T -> @T -> real
GetAverageAux(s)(sum)(numberOfElem) ==
 if is_(s,seq of real) and is_real(sum) and is_real(numberOfElem)
 then
	cases s :
	[h] ^ tail	-> GetAverageAux[@T](tail)(sum + h)(numberOfElem),
	[]			-> sum / numberOfElem
	end
else undefined;
--measure length_measure;

static public isAscendingTotalOrder [@T]:
	(@T * @T -> bool) -> seq of @T -> bool
isAscendingTotalOrder (decideOrderFunc)(s) ==
	forall i,j  in set inds s & i < j  => decideOrderFunc(s(i),s(j)) or s(i) = s(j);

static public isDescendingTotalOrder [@T]:
	(@T * @T -> bool) -> seq of @T -> bool
isDescendingTotalOrder (decideOrderFunc)(s) ==
	forall i,j  in set inds s & i < j  => decideOrderFunc(s(j),s(i)) or s(i) = s(j);

static public isAscendingOrder [@T]: seq of @T -> bool
isAscendingOrder(s) ==
	isAscendingTotalOrder [@T](lambda x : @T, y : @T & if is_real(x) and is_real(y)
                                                     then x < y
                                                     else undefined)(s);

static public isDescendingOrder[@T]: seq of @T -> bool
isDescendingOrder(s) ==
	isDescendingTotalOrder [@T](lambda x : @T, y : @T & if is_real(x) and is_real(y)
                                                      then x < y
                                                      else undefined)(s);

static public sort[@T] : (@T * @T -> bool) -> seq of @T -> seq of @T
sort(decideOrderFunc)(s) ==
	cases s:
		[]	-> [],
		[h]^tail	-> 
			sort[@T](decideOrderFunc)([tail(i) | i in set inds tail & decideOrderFunc(tail(i),h)]) ^
			[h] ^
			sort[@T](decideOrderFunc)([tail(i) | i in set inds tail & not decideOrderFunc(tail(i),h)])
	end;

static public ascendingOrderSort[@T] : seq of @T -> seq of @T
ascendingOrderSort(s) == sort[@T](lambda x : @T, y : @T & if is_real(x) and is_real(y)
                                                          then x < y
                                                          else undefined)(s);

static public descendingOrderSort[@T] : seq of @T -> seq of @T
descendingOrderSort(s) == sort[@T](lambda x : @T, y : @T & if is_real(x) and is_real(y)
                                                           then x > y
                                                           else undefined)(s);

static public isOrdered[@T] : seq of (@T * @T -> bool) -> seq of @T -> seq of @T -> bool
isOrdered(decideOrderFuncSeq)(s1)(s2) ==
	cases mk_(s1,s2):
		mk_([],[])		-> false,
		mk_([],-)		-> true,
		mk_(-,[])	-> false,
		mk_([h1]^tail1,[h2]^tail2)	->
			if (hd decideOrderFuncSeq)(h1,h2) then
				true
			elseif (hd decideOrderFuncSeq)(h2,h1) then
				false
			else
				Sequence`isOrdered[@T](tl decideOrderFuncSeq)(tail1)(tail2)
	end;

static public Merge[@T] : (@T * @T -> bool) -> seq of @T -> seq of @T -> seq of @T
Merge(decideOrderFunc)(s1)(s2) == 
	cases mk_(s1,s2):
		mk_([], y)						-> y,
		mk_(x, [])						-> x,
		mk_([h1]^tail1,[h2]^tail2)		->
			if decideOrderFunc(h1,h2) then
				[h1] ^ Sequence`Merge[@T](decideOrderFunc)(tail1)(s2)
			else
				[h2] ^ Sequence`Merge[@T](decideOrderFunc)(s1)(tail2)
	end;

static public InsertAt[@T]: nat1 -> @T -> seq of @T -> seq of @T
InsertAt(position)(e)(s) ==
	cases mk_(position, s) :
	mk_(1, str)				-> [e] ^ str,
	mk_(-, [])				-> [e],
	mk_(pos, [h] ^ tail)	-> [h] ^ InsertAt[@T](pos - 1)(e)(tail)
	end;

static public RemoveAt[@T]: nat1 -> seq of @T -> seq of @T
RemoveAt(position)(s) ==
	cases mk_(position, s) :
	mk_(1, [-] ^ tail)		-> tail,
	mk_(pos, [h] ^ tail)	-> [h] ^ RemoveAt[@T](pos - 1)(tail),
	mk_(-, [])				-> []
	end;

static public RemoveDup[@T] :  seq of @T ->  seq of @T
RemoveDup(s) == 
	cases s :
	[h]^tail		-> [h] ^ RemoveDup[@T](filter[@T](lambda x : @T & x <> h)(tail)) ,
	[]			-> []
	end
measure length_measure;
	
static public RemoveMember[@T] :  @T -> seq of @T -> seq of @T
RemoveMember(e)(s) == 
	cases s :
	[h]^tail		-> if e = h then tail else [h] ^ RemoveMember[@T](e)(tail),
	[]			-> []
	end;
	
static public RemoveMembers[@T] :  seq of @T -> seq of @T -> seq of @T
RemoveMembers(elemSeq)(s) == 
	cases elemSeq :
	[]			-> s,
	[h]^tail		-> RemoveMembers[@T](tail)(RemoveMember[@T](h)(s))
	end;

static public UpdateAt[@T]: nat1 -> @T -> seq of @T -> seq of @T
UpdateAt(position)(e)(s) ==
	cases mk_(position, s) :
	mk_(-, [])				-> [],
	mk_(1, [-] ^ tail)		-> [e] ^ tail,
	mk_(pos,  [h] ^ tail)	-> [h] ^ UpdateAt[@T](pos - 1)(e)(tail)
	end;

static public take[@T]: int -> seq of @T -> seq of @T
take(i)(s) == s(1,...,i);

static public TakeWhile[@T] : (@T -> bool) -> seq of @T ->seq of @T
TakeWhile(f)(s) ==
	cases s :
	[h] ^ tail	-> 
		if f(h) then
			[h] ^ TakeWhile[@T](f)(tail)
		else
			[],
	[]	-> []
	end;
	
static public drop[@T]: int -> seq of @T -> seq of @T
drop(i)(s) == s(i+1,...,len s);

static public DropWhile[@T] : (@T -> bool) -> seq of @T ->seq of @T
DropWhile(f)(s) ==
	cases s :
	[h] ^ tail	-> 
		if f(h) then
			DropWhile[@T](f)(tail)
		else
			s,
	[]	-> []
	end;

static public Span[@T] : (@T -> bool) -> seq of @T -> seq of @T * seq of @T
Span(f)(s) ==
	cases s :
	[h] ^ tail	-> 
		if f(h) then
			let	mk_(matchSeq, otherSeq) = Span[@T](f)(tail)
			in
			mk_([h] ^ matchSeq, otherSeq)
		else
			mk_([], s),
	[]	-> mk_([], [])
	end;

static public SubSeq[@T]: nat -> nat -> seq1 of @T -> seq of @T
SubSeq(startPos)(numOfElem)(s) == s(startPos,...,startPos+numOfElem-1);

static public last[@T]: seq of @T -> @T
last(s) == s(len s);

static public fmap[@T1,@T2]: (@T1 -> @T2) -> seq of @T1 -> seq of @T2
fmap(f)(s) == [f(s(i)) | i in set inds s];

public Fmap[@elem]: (@elem -> @elem) -> seq of @elem -> seq of @elem
Fmap(f)(l) ==
       if l = []
       then []
       else [f(hd l)] ^ (Fmap[@elem](f)(tl l));

static public filter[@T]: (@T -> bool) -> seq of @T -> seq of @T
filter(f)(s) == [s(i) | i in set inds s & f(s(i))];

static public Foldl[@T1, @T2] : 
	(@T1 -> @T2 -> @T1) -> @T1 -> seq of @T2 -> @T1
Foldl(f)(arg)(s) == 
	cases s :
	[]			-> arg,
	[h] ^ tail	-> Foldl[@T1,@T2](f)(f(arg)(h))(tail)
	end;

static public Foldr[@T1, @T2] : 
	(@T1 -> @T2 -> @T2) -> @T2 -> seq of @T1 -> @T2
Foldr(f)(arg)(s) == 
	cases s :
	[]			-> arg,
	[h] ^ tail	-> f(h)(Foldr[@T1,@T2](f)(arg)(tail))
	end;

static public isMember[@T] : @T -> seq of @T -> bool
isMember(e)(s) == 
	cases s :
	[h]^tail		-> e = h or isMember[@T] (e)(tail),
	[]			-> false
	end;

static public isAnyMember[@T]:  seq of @T -> seq of @T -> bool
isAnyMember(elemSeq)(s) == 
	cases elemSeq :
	[h]^tail		->  isMember[@T] (h)(s) or isAnyMember[@T] (tail)(s) ,
	[]			-> false
	end;

static public Index[@T]: @T -> seq of @T -> int
Index(e)(s) == 
	let	i = 0
	in	IndexAux[@T](e)(s)(i);

static IndexAux[@T]: @T -> seq of @T -> int -> int
IndexAux(e)(s)(indx) ==
	cases s:
		[]			-> 0,
		[x]^xs	->
			if x = e then 
				indx + 1
			else
				IndexAux[@T](e)(xs)(indx+1)
	end;
	
static public IndexAll2[@T] : @T -> seq of @T -> set of int
IndexAll2(e)(s) == {i | i in set inds s & s(i) = e};
	
static public flatten[@T] : seq of seq of @T -> seq of @T
flatten(s) == conc s;

static public compact[@T] : seq of [@T] -> seq of @T
compact(s) == [s(i) | i in set inds s & s(i) <> nil];

static public freverse[@T] : seq of @T -> seq of @T
freverse(s) == [s(len s + 1 -  i) | i in set inds s];

static public Permutations[@T]: seq of @T -> set of seq of @T
Permutations(s) == 
cases s:
	[],[-] -> {s},
	others -> dunion {{[s(i)]^j | j in set Permutations[@T](RestSeq[@T](s,i))} | i in set inds s}
end
measure length_measure;

static public RestSeq[@T]: seq of @T * nat -> seq of @T
RestSeq(s,i) == [s(j) | j in set (inds s \ {i})];

static public Unzip[@T1, @T2] : seq of (@T1 * @T2) -> seq of @T1 * seq of @T2
Unzip(s) ==
	cases s :
	[]				-> mk_([], []),
	[mk_(x, y)] ^ tail	->
		let	mk_(xs, ys) = Unzip[@T1, @T2](tail)
		in
		mk_([x] ^ xs, [y] ^ ys)
	end
measure lengthUnzip;

static lengthUnzip[@T1, @T2] : seq of (@T1 * @T2) +> nat
lengthUnzip(s) == len s;

static public Zip[@T1, @T2] : seq of @T1 * seq of @T2 -> seq of (@T1 * @T2)
Zip(s1, s2) == Zip2[@T1, @T2](s1)(s2);
                            	
static public Zip2[@T1, @T2] : seq of @T1 -> seq of @T2 -> seq of (@T1 * @T2)
Zip2(s1)(s2) == 
	cases mk_(s1, s2) :
	mk_([h1] ^ tail1, [h2] ^ tail2)		-> [mk_(h1, h2)] ^ Zip2[@T1, @T2](tail1)(tail2),
	mk_(-, -)							-> []
	end;

end Sequence
                                                                       

AllT.vdmpp

/*
Test Group
	Test of all test cases
Written by
	Shin Sahara
*/
class AllT
operations
public run : () ==>bool
run () == 
	let	ResultOfTest =
		[
			new TermT().run(),
			new TimeT().run(),
			new MapT().run(),
			new HashtableT().run(),
			new FHashtableT().run(),
			new DoubleListQueueT().run(),
			new QueueT().run(),
			new UniqueNumberT().run(),
			new RealT().run(), 
			new SetT().run(),
			new SequenceT().run(),
			new StringT().run(),
			new IntegerT().run(),
			new NumberT().run(),
			new CalendarT().run(),
			new SBCalendarT().run(),
			new DateT().run(),
			new FunctionT().run()
			],
		Message = "Result of all test cases."
		
	in
	if   forall i in set inds ResultOfTest & ResultOfTest(i) then
		return new TestLogger().succeededInAllTestcases(Message)
	else
		return new TestLogger().notSucceededInAllTestcases(Message)
	
end AllT
 

Function.vdmpp

              
class Function

functions 
                            
static public Funtil[@T] : (@T -> bool) -> (@T -> @T) -> @T -> @T
Funtil(p)(f)(x) == if p(x) then x else Funtil[@T](p)(f)(f(x));
                            
static public Fwhile[@T] : (@T -> bool) -> (@T -> @T) -> @T -> @T
Fwhile(p)(f)(x) == if p(x) then Fwhile[@T](p)(f)(f(x)) else x;
                            
static public Seq[@T] : seq of (@T -> @T) -> @T -> @T
Seq(fs)(p) ==
	cases fs :
	[xf] ^ xfs	-> Seq[@T](xfs)(xf(p)),
	[]					-> p
	end
--measure length
;

--static length[@T] : seq of (@T -> @T) -> @T -> nat
--length(fs)(-) == len fs;
                            
static public readFn[@T] : seq of char -> [@T]
readFn(fname) ==
	let 
		io = new IO(),
		mk_(aResult, f) = io.freadval[@T](fname)
	in
	if aResult then
		f
	else
		let -= io.echo("Can't read values from the data file = " ^ fname)
		in
		nil;
                            
end Function
            

HashtableT.vdmpp

/*
Test Group 
	test of Hashtable
*/
----------------------------------------------------
class StringObj is subclass of CommonDefinition

instance variables
public content : seq of char;

functions
public hashCode : () -> int
hashCode() == 
	let c = getContent() in
	if  c <> nil then
		len c mod 17
	else
		-1;

public equals : Object -> bool
equals(anObject) == if isofclass(StringObj, anObject)
                   then self.getContent() = anObject.getContent()
                   else false;

operations
public StringObj : seq of char ==> StringObj
StringObj(aString) ==
	(
	content := aString;
	return self
	);

public getContent : () ==> [seq of char]
getContent() == 
	if isofclass(StringObj, self) then 
		return content
	else 
		return nil;

end StringObj
----------------------------------------------------
class IntObj is subclass of CommonDefinition

instance variables
public content : int;

functions
public hashCode : () -> int
hashCode() == 
	let c = getContent() in
	if c <> nil then
		c mod 13
	else
		-1;

public equals : Object -> bool
equals(anObject) == if isofclass(IntObj, anObject)
                   then self.getContent() = anObject.getContent()
                   else false;

operations
public IntObj : int ==> IntObj
IntObj(i) ==
	(
	content := i;
	return self
	);
	
public getContent : () ==> [int]
getContent() == 
	if isofclass(IntObj, self) then 
		return content
	else 
		return nil;

end IntObj
----------------------------------------------------
class HashtableT is subclass of TestDriver
functions
public tests : () -> seq of TestCase
tests() == 
	[ 
	new HashtableT52(), new HashtableT53(), new HashtableT54(),
	new HashtableT55(), new HashtableT56(), new HashtableT57(),
	new HashtableT01(), new HashtableT02(), new HashtableT03(),
	new HashtableT04(), 
	new HashtableT05(), new HashtableT06(),
	new HashtableT07()
	];
end HashtableT
----------------------------------------------------

class HashtableT01 is subclass of TestCase, CommonDefinition
operations 

protected test: () ==> bool
test() == 
	let	h1 = new Hashtable(),
		k1 = new IntObj(1),
		k2 = new IntObj(2),
		k3 = new IntObj(3),
		h2 =
			new Hashtable({
				k1 |-> new StringObj("Shin Sahara"), 
				k2 |-> new StringObj("Kei Sato"), 
				k3 |-> new StringObj("Hiroshi Sakoh")
			})
	in
	return 
		h1.getBuckets() = { |-> } and
		h2.get(k1).equals(new StringObj("Shin Sahara")) and
		h2.get(k2).equals(new StringObj("Kei Sato")) and
		h2.get(k3).equals(new StringObj("Hiroshi Sakoh")) and
		h2.get(new IntObj(1)).equals(new StringObj("Shin Sahara")) and
		h2.get(new IntObj(2)).equals(new StringObj("Kei Sato")) and
		h2.get(new IntObj(3)).equals(new StringObj("Hiroshi Sakoh")) 
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT01:\tConstructor test.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT01
---------------------------------------

class HashtableT02 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	h1 = 
			new Hashtable({
				new IntObj(1) |-> new StringObj("Shin Sahara"), 
				new IntObj(2) |->new StringObj("Kei Sato"), 
				new IntObj(3) |-> new StringObj("Hiroshi Sakoh")
			}),
		h2 = 
			new Hashtable({
				new StringObj("a") |->new IntObj(1),  
				new StringObj("b") |-> new IntObj(2), 
				new StringObj("c") |-> new IntObj(3)
			})
	in
	return 
		h1.contains(new StringObj("Shin Sahara")) and
		h1.contains(new StringObj("Kei Sato")) and
		h1.contains(new StringObj("Shin Sakoh")) = false and
		h1.containsKey(new IntObj(1)) and
		h1.containsKey(new IntObj(4)) = false and
		h2.contains(new IntObj(3)) and
		h2.contains(new IntObj(7)) = false and
		h2.containsKey(new StringObj("a")) and
		h2.containsKey(new StringObj("d")) = false
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT02:\tsearch test.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT02
---------------------------------------

class HashtableT03 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	h1 =
			new Hashtable({
				new IntObj(1) |-> new StringObj("Shin Sahara"), 
				new IntObj(2) |->new StringObj("Kei Sato"), 
				new IntObj(3) |-> new StringObj("Hiroshi Sakoh")
			}),
		h2 = 
			new Hashtable({
				new StringObj("a") |->new IntObj(1),  
				new StringObj("b") |-> new IntObj(2), 
				new StringObj("c") |-> new IntObj(3)
			}),
		deleteObj = h2.remove(new StringObj("b"))
	in
	(
	h1.clear();
	return 
		h1.getBuckets() = {|->} and
		deleteObj.equals(new IntObj(2)) and
		h2.get(new StringObj("b")) = nil and
		h2.contains(new IntObj(2)) = false and
		h2.containsKey(new StringObj("b")) = false and
		h2.remove(new StringObj("d")) = nil
	)
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT03:\tDelete test.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT03
---------------------------------------

class HashtableT04 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	--let	h1 = new Hashtable(),
	--	h2 = new Hashtable()
	--in
	(
	dcl h1 : Hashtable := new Hashtable();
	dcl h2 : Hashtable := new Hashtable();
	h1.putAll({
			new IntObj(1) |-> new StringObj("Shin Sahara"), 
			new IntObj(2) |->new StringObj("Kei Sato"), 
			new IntObj(14) |-> new StringObj("Hiroshi Sakoh")
	});
	h2.put(new StringObj("a"), new IntObj(1));
	h2.put(new StringObj("b"), new IntObj(2));
	def c = new StringObj("c") in (
		h2.put(c, new IntObj(4));
		h2.put(c, new IntObj(3))
	);
	return
		h1.get(new IntObj(1)).equals(new StringObj("Shin Sahara"))  and
		h1.get(new IntObj(2)).equals(new StringObj("Kei Sato")) and
		h1.get(new IntObj(14)).equals(new StringObj("Hiroshi Sakoh")) and
		h1.get(new IntObj(4)) = nil and  
		h2.get(new StringObj("a")).equals(new IntObj(1)) and
		h2.get(new StringObj("b")).equals(new IntObj(2)) and
		h2.get(new StringObj("c")).equals(new IntObj(3)) and 
		h2.get(new StringObj("d")) = nil 
	)
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT04:\tTest of put, get.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT04
---------------------------------------

class HashtableT05 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	h1 = new Hashtable(),
		h2 = new Hashtable(),
		h1k1 = new IntObj(1),
		h1k2 = new IntObj(2),
		h1k3 = new IntObj(14),
		h1v1 = new StringObj("Shin Sahara"),
		h1v2 = new StringObj("Kei Sato"),
		h1v3 = new StringObj("Hiroshi Sakoh"),
		h2k1 = new StringObj("a"),
		h2k2 = new StringObj("b"),
		h2k3 = new StringObj("c"),
		h2v1 = new IntObj(1),
		h2v2 = new IntObj(2),
		h2v3 = new IntObj(18)
		
	in
	(
	h1.putAll({
			h1k1 |-> h1v1, 
			h1k2 |-> h1v2, 
			h1k3 |-> h1v3
	});
	h2.put(h2k1, h2v1);
	h2.put(h2k2, h2v2);
	h2.put(h2k3, h2v3);
	let	keySet1 = h1.keySet(),
		valueSet1 = h1.valueSet(),
		keySet2 = h2.keySet(),
		valueSet2 = h2.valueSet()
	in
	return
		keySet1 = {h1k1, h1k2, h1k3} and
		valueSet1 = {h1v1, h1v2, h1v3} and
		keySet2 = {h2k1, h2k2, h2k3} and
		valueSet2 = {h2v1, h2v2, h2v3}
	)
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT05:\tTest of getting keys and values.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT05
---------------------------------------

class HashtableT06 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	h1 = new Hashtable(),
		h1k1 = new IntObj(1),
		h1k2 = new IntObj(14),
		h1k3 = new IntObj(16),
		h1k4 = new IntObj(27),
		h1v1 = new StringObj("a"),
		h1v2 = new StringObj("b"),
		h1v3 = new StringObj("c")
	in
	(
	h1.putAll({
			h1k1 |-> h1v1, 
			h1k2 |-> h1v2, 
			h1k3 |-> h1v3
	});
	let	- = h1.remove(new IntObj(14)) 
	in
	h1.put(h1k4, h1v3);
	return
		h1.keySet() = {h1k1, h1k3, h1k4} and
		h1.valueSet() = {h1v1, h1v3, h1v3}
	)
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT06:\tTest when hashCode overlaps.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT06
---------------------------------------

class HashtableT07 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	h1 = new Hashtable(),
		h2 = new Hashtable(),
		h1k1 = new IntObj(1),
		h1k2 = new IntObj(14),
		h1k3 = new IntObj(16),
		h1v1 = new StringObj("a"),
		h1v2 = new StringObj("b"),
		h1v3 = new StringObj("c")
	in
	(
	h1.putAll({
			h1k1 |-> h1v1, 
			h1k2 |-> h1v2, 
			h1k3 |-> h1v3
	});
	h2.putAll({
			h1k1 |-> h1v1, 
			h1k2 |-> h1v2, 
			h1k3 |-> h1v3
	});
	let	- = h1.remove(new IntObj(1)),
		- = h1.remove(new IntObj(14)),
		- = h1.remove(new IntObj(16)),
		- = h2.remove(new IntObj(14))
	in
	return
		h1.isEmpty() and
		h1.size() = 0 and
		h2.isEmpty() = false and
		h2.size() = 2 
		
	)
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT07:\tTest of size.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT07
---------------------------------------

class HashtableT52 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	aHashCode = lambda x : int & x mod 13,
		p1 = Hashtable`PutAll[int, seq of char]({ |-> })(aHashCode)(
				{1 |-> "Sahara", 2 |-> "Sato", 14 |-> "Sakoh"}
			),
		c1 = Hashtable`Contains[int, seq of char](p1)
	in
	return
		c1("Sahara") and
		c1("Sato") and
		c1("Sakoh") and
		c1("") = false
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT52:\tFunctional finding.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT52
---------------------------------------

class HashtableT53 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	aHashCode1 = lambda x : int & x mod 13,
		aHashCode2 = lambda x : seq of char & if x = "" then "" else Sequence`take[char](1)(x),
		- = Hashtable`PutAll[int, seq of char]({ |-> })(aHashCode1)(
				{1 |-> "Shin Sahara", 2 |-> "Kei Sato", 14 |-> "Hiroshi Sakoh"}
			),
		h2 = Hashtable`PutAll[seq of char, int]({ |-> })(aHashCode2)(
				{"a" |-> 1, "b" |-> 2, "c" |-> 3}
			),
		h3 = Hashtable`Clear[int, seq of char](),
		afterRemoveh2 = Hashtable`Remove[seq of char, int](h2)(aHashCode2)("b"),
		c1 = Hashtable`Contains[seq of char, int](afterRemoveh2),
		ck1 = Hashtable`ContainsKey[seq of char, int](afterRemoveh2)
	in
	(
	return 
		h3 = {|->} and
		Hashtable`Get[seq of char, int](afterRemoveh2)(aHashCode2)("b") = nil and
		c1(2) = false and
		c1(1) and
		c1(3) and
		ck1("b") = false and 
		ck1("a") and
		ck1("c") 
	)
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT53:\tTest of functional remove.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT53
---------------------------------------

class HashtableT54 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	aHashCode = lambda x : int & x mod 13,
		put = Hashtable`Put[int, seq of char],
		p1 = put({ |-> })(aHashCode)(1)("Sahara"),
		p2 = put(p1)(aHashCode)(2)("Bush"),
		p3 = put(p2)(aHashCode)(2)("Sato"),
		p4 = put(p3)(aHashCode)(14)("Sakoh"),
		get = Hashtable`Get[int, seq of char](p4)
	in
	return
		get(aHashCode)(1) = "Sahara" and
		get(aHashCode)(2) = "Sato" and
		get(aHashCode)(14) = "Sakoh" and
		get(aHashCode)(99) = nil
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT54:\tFunctional Put and Get.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT54
---------------------------------------

class HashtableT55 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	aHashCode = lambda x : int & x mod 13,
		put = Hashtable`Put[int, seq of char],
		p1 = put({ |-> })(aHashCode)(1)("Sahara"),
		p2 = put(p1)(aHashCode)(2)("Bush"),
		p3 = put(p2)(aHashCode)(2)("Sato"),
		p4 = put(p3)(aHashCode)(14)("Sakoh"),
		k = Hashtable`KeySet[int, seq of char],
		v = Hashtable`ValueSet[int, seq of char]
	in
	return
		k(p1) = {1} and
		v(p1) = {"Sahara"} and
		k(p2) = {1, 2} and
		v(p2) = {"Sahara", "Bush"} and
		k(p4) = {1,2,14} and
		v(p4) = {"Sahara", "Sato", "Sakoh"}
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT55:\tFunctional getting information.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT55
---------------------------------------

class HashtableT56 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	aHashCode1 = lambda x : int & x mod 13,
		h1 = Hashtable`PutAll[int, seq of char]({ |-> })(aHashCode1)(
				{1 |-> "Shin Sahara", 2 |-> "Kei Sato", 14 |-> "Hiroshi Sakoh", 27 |-> "Nishikawa"}
			),
		h2 = Hashtable`Remove[int, seq of char](h1)(aHashCode1)(14)
	in
	(
	return
		Hashtable`KeySet[int, seq of char](h2) = {1, 2, 27} and
		Hashtable`ValueSet[int, seq of char](h2) = {"Shin Sahara",  "Kei Sato", "Nishikawa"}
	)
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT56:\tWhen hashode overlapped.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT56
---------------------------------------

class HashtableT57 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	aHashCode1 = lambda x : int & x mod 13,
		remove = Hashtable`Remove[int, seq of char],
		h1 = Hashtable`PutAll[int, seq of char]({ |-> })(aHashCode1)(
				{1 |-> "Shin Sahara", 2 |-> "Kei Sato", 14 |-> "Hiroshi Sakoh"}
			),
		h2 = remove(h1)(aHashCode1)(1),
		h3 = remove(h2)(aHashCode1)(2),
		h4 = remove(h3)(aHashCode1)(14),
		isempty = Hashtable`IsEmpty[int, seq of char],
		size = Hashtable`Size[int, seq of char]
	in
	(
	return
		isempty(h4) and
		size(h4) = 0 and
		isempty(h3)  = false and
		size(h3) = 1 and
		size(h2) = 2 and
		size(h1) = 3
	)
;
protected setUp: () ==> ()
setUp() == TestName := "HashtableT57:\tTest of functional Size.";
protected tearDown: () ==> ()
tearDown() == return;
end HashtableT57
---------------------------------------

ProductT.vdmpp

class ProductT is subclass of TestDriver 
functions
public tests : () -> seq of TestCase
tests() == 
	[ 
	new ProductT01()
	];
end ProductT
----------------------------------------------------------

class ProductT01 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	lt = String`LT,
		lt2 = lambda x : int, y : int & x < y
	in
	return
		Product`Curry[seq of char, seq of char, bool](lt)("abc")("abcd") and
		Product`Curry[seq of char, seq of char, bool](lt)("abcde")("abcd") = false and
		Product`Curry[int, int, bool](lt2)(3)(4) and
		Product`Uncurry[seq of char, seq of char, bool](String`LT2)("abc", "abcd") and
		Product`Uncurry[seq of char, seq of char, bool](String`LT2)("abcde", "abcd") = false and
		Product`Uncurry[seq of char, seq of char, bool](String`LE2)("3", "4")
	;
protected setUp: () ==> ()
setUp() == TestName := "ProductT01:\t Test of curry function.";
protected tearDown: () ==> ()
tearDown() == return;
end ProductT01

Map.vdmpp

class Map 

functions
static public Get[@T1, @T2] : map @T1 to @T2 -> @T1 -> [@T2]
Get(aMap)(aKey) ==
	if aKey in set dom aMap then
		aMap(aKey)
	else
		nil;

static public Contains[@T1, @T2] : map @T1 to @T2 -> @T2 -> bool
Contains(aMap)(aValue) == aValue in set rng aMap;

static public ContainsKey[@T1, @T2] : map @T1 to @T2 -> @T1 -> bool
ContainsKey(aMap)(aKey) == aKey in set dom aMap;
	
end Map

CalendarT.vdmpp

class CalendarT is subclass of TestDriver 
functions
public tests : () -> seq of TestCase
tests() == 
	[
	new CalendarT12(),
	new CalendarT11(),
	new CalendarT10(),
	new CalendarT09(),
	--new CalendarT08(), --deleted
	new CalendarT07(),
	new CalendarT06(),
	new CalendarT05(),
	new CalendarT03(),
	new CalendarT02(), 
	new CalendarT01(),
	new CalendarT04()
	];
end CalendarT

class CalendarT01 is subclass of TestCase
operations 
protected test: () ==> bool
	test() == 
		let	jc = new JapaneseCalendar()	in
	(
	jc.setToday(jc.getDateFrom_yyyy_mm_dd(2001,9,12));
	return
		jc.getDateFrom_yyyy_mm_dd(2003, 3, 0).asString() = "20030228" and
		jc.getDateFrom_yyyy_mm_dd(2003, 2, 29).asString() = "20030301" and
		jc.getDateFrom_yyyy_mm_dd(2004, 3, 0).asString() = "20040229" and
		jc.getDateFrom_yyyy_mm_dd(2004, 2, 30).asString() = "20040301" and
		jc.getDateFrom_yyyy_mm_dd(2004, 1, 60).asString() = "20040229" and
		jc.getDateFrom_yyyy_mm_dd(2004, 1, 61).asString() = "20040301" and
		jc.getDateFrom_yyyy_mm_dd(2001,5,1).get_yyyy_mm_dd() = mk_(2001,5,1) and
		jc.getYyyymmdd(jc.today()) = mk_(2001,9,12) and
		jc.modifiedJulianDate2Date(jc.julianDate2ModifiedJulianDate(2299160)).get_yyyy_mm_dd() = mk_(1582,10,4)  and	--theDayBeforeGregorioCalendarStarted
		jc.modifiedJulianDate2Date(jc.julianDate2ModifiedJulianDate(2299160)).plus(1).get_yyyy_mm_dd() = mk_(1582,10,15) and	--theFirstDayOfGregorioCalendar
		jc.date2Str(jc.getDateFromString("20010711")) = "20010711" and
		jc.convertDateFromString("saharashin") = nil and
		JapaneseCalendar`getJapaneseDateStr(jc.getDateFrom_yyyy_mm_dd(2001,5,1)) = "13 5 1" and
		jc.getAutumnalEquinox(2001).EQ(jc.getDateFrom_yyyy_mm_dd(2001,9,23)) = true
	)
	;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT01:\tMake date.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT01

class CalendarT02 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar()	in
	return
		jc.dateAdding(jc.getDateFrom_yyyy_mm_dd(2001,5,1),3) .date2Str() = "20010504" and
		jc.diffOfDates(jc.getDateFrom_yyyy_mm_dd(2001,5,8),jc.getDateFrom_yyyy_mm_dd(2001,5,1)) = 7 and
		jc.dateSubtracting(jc.getDateFrom_yyyy_mm_dd(2001,5,1),1) .get_yyyy_mm_dd() = mk_(2001,4,30)
;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT02:\tAddition and subtraction of date.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT02

class CalendarT03 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar()	in
	return
		jc.getVernalEquinox(2001).date2Str() = "20010320" and
		jc.getSummerSolstice(2001).date2Str() = "20010621" and
		jc.getAutumnalEquinox(2001).date2Str() = "20010923" and
		jc.getWinterSolstice(2001).date2Str() = "20011222" and
		jc.getVernalEquinox(2999).date2Str() = "29990320" and
		jc.getSummerSolstice(2999).date2Str() = "29990620" and
		jc.getAutumnalEquinox(2999).date2Str() = "29990922" and
		jc.getWinterSolstice(2999).date2Str() = "29991222" and
		--jc.getWinterSolstice(2008).date2Str() = "20081221" and -- error in leap year
		jc.getWinterSolstice(2007).date2Str() = "20071222" and
		jc.getWinterSolstice(2012).date2Str() = "20121221" and
		jc.getWinterSolstice(2016).date2Str() = "20161221" 
	;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT03:\tCalculation of Vernal Equinox, Summer Solstice, Autumnal Equinox, Winter Solstice.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT03

class CalendarT04 is subclass of TestCase
operations 
public test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar(),
		setOfDayOffIn2009 = jc.getSetOfDayOff(2009),
		setOfDayOff = jc.getSetOfDayOff(2001),
		setOfDayOff2003 = jc.getSetOfDayOff(2003),
		d0401 = jc.getDateFromString("20010401"),
		d0408 = jc.getDateFromString("20010408"),
		d0430 = jc.getDateFromString("20010430"),
		setOfDayOffBy_yyyy_mm_dd =  {jc.getYyyymmdd(dayOff) | dayOff in set setOfDayOff},
		setOfDayOffBy_yyyy_mm_dd2003 =  {jc.getYyyymmdd(dayOff) | dayOff in set setOfDayOff2003},
		setOfDayOffBy_yyyy_mm_ddIn2009 =  {jc.getYyyymmdd(dayOff) | dayOff in set setOfDayOffIn2009}
		in
	return
		setOfDayOffBy_yyyy_mm_dd = 
			{ mk_( 2001,1,1 ),
  			mk_( 2001,1,8 ),
			mk_( 2001,2,11 ),
 			mk_( 2001,2,12 ),
  			mk_( 2001,3,20 ),
 			mk_( 2001,4,29 ),
  			mk_( 2001,4,30 ),
  			mk_( 2001,5,3 ),
  			mk_( 2001,5,4 ),
  			mk_( 2001,5,5 ),
 			mk_( 2001,7,20 ),
  			mk_( 2001,9,15 ),
			mk_( 2001,9,23 ),
  			mk_( 2001,9,24 ),
  			mk_( 2001,10,8 ),
  			mk_( 2001,11,3 ),
  			mk_( 2001,11,23 ),
  			mk_( 2001,12,23 ),
  			mk_( 2001,12,24 )
  			} and
  		setOfDayOffBy_yyyy_mm_dd2003 =
  			{ mk_( 2003,1,1 ),
			  mk_( 2003,1,13 ),
			  mk_( 2003,2,11 ),
			  mk_( 2003,3,21 ),
			  mk_( 2003,4,29 ),
			  mk_( 2003,5,3 ),
			  mk_( 2003,5,4 ),
			  mk_( 2003,5,5 ),
			  mk_( 2003,7,21 ),
			  mk_( 2003,9,15 ),
			  mk_( 2003,9,23 ),
			  mk_( 2003,10,13 ),
			  mk_( 2003,11,3 ),
			  mk_( 2003,11,23 ),
			  mk_( 2003,11,24 ),
 			  mk_( 2003,12,23 ) 
 			 } and
		setOfDayOffBy_yyyy_mm_ddIn2009 =
			  { mk_( 2009, 1, 1 ),
				mk_( 2009, 1, 12 ),
				mk_( 2009, 2, 11 ),
				mk_( 2009, 3, 20 ),
				mk_( 2009, 4, 29 ),
				mk_( 2009, 5, 3 ),
				mk_( 2009, 5, 4 ),
				mk_( 2009, 5, 5 ),
				mk_( 2009, 5,6 ),
				mk_( 2009, 7, 20 ),
				mk_( 2009, 9, 21 ),
  				mk_( 2009, 9, 22 ),
				mk_( 2009, 9, 23 ),
				mk_( 2009, 10, 12 ),
				mk_( 2009, 11, 3 ),
				mk_( 2009, 11, 23 ),
				mk_( 2009, 12, 23 ) } and
  		jc.getDayOffsExceptSunday(d0401,d0430)  = 2 and
  		card jc.getDayOffsAndSunday(d0401,d0430) = 1 and
  		jc.getDayOffsAndSunday(d0401,d0408) = {}
	;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT04:\tGet set of Day off.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT04

class CalendarT05 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar(),
		d0711 = jc.getDateFromString("20010711")	in
	(
	jc.setToday(jc.getDateFrom_yyyy_mm_dd(2001,3,1));
	let	d0301 = jc.today()	in
	return
		d0711.EQ(jc.getDateFrom_yyyy_mm_dd(2001, 7, 11)) and
		jc.EQ(d0711,jc.getDateFrom_yyyy_mm_dd(2001, 7, 11)) and
		d0301.LT(d0711) and
		jc.LT(d0301, d0711) and
		d0711.GT(d0301) and
		jc.GT(d0711,d0301) and
		d0711.GE(d0711) and d0711.GE(d0301) and
		jc.GE(d0711,d0711)  and jc.GE(d0711,d0301) and
		d0711.LE(d0711) and d0301.LE(d0711) and
		jc.LE(d0711,d0711) and jc.LE(d0301,d0711) 
	)
;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT05:\tCompare date.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT05

class CalendarT06 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar(),
		d10010301 = jc.getDateFromString("10010301"),
		d0711 = jc.getDateFromString("20010711")		in
	(
	let	d0301 = jc.today()	in
	return
		jc.firstDayOfTheWeekInMonth(2000,3,<Wed>).get_yyyy_mm_dd() = mk_( 2000,3,1 ) and
		jc.firstDayOfTheWeekInMonth(2001,7,<Sun>).get_yyyy_mm_dd() = mk_( 2001,7,1 ) and
		jc.lastDayOfTheWeekInMonth(2000,2,<Tue>).get_yyyy_mm_dd() = mk_( 2000,2,29 ) and
		jc.lastDayOfTheWeekInMonth(2001,7,<Sun>).get_yyyy_mm_dd() = mk_( 2001,7,29 ) and
		jc.getNthDayOfTheWeek(2001,7,5,<Sun>).get_yyyy_mm_dd() = mk_( 2001,7,29 ) and
		jc.getNthDayOfTheWeek(2001,7,6,<Sun>) = false and
		jc.getNumberOfTheDayOfWeek(d0711,d0301,<Sun>)  = 19 and
		jc.getNumberOfTheDayOfWeek(d0711,d10010301,<Sun>)  = 52196 and
		jc.getNumberOfDayOfTheWeekFromName(<Thu>) = 4 and
		jc.getNumberOfDayOfTheWeekFromName(<Fri>) = 5 and
		jc.getNumberOfDayOfTheWeekFromName(<Sat>) = 6 and
		jc.getNumberOfDayOfTheWeekFromName(<Sun>) = 0 
	)
	;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT06:\tGet day of the week.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT06

class CalendarT07 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar()	in
	return
		jc.getDateFromString("sahara") = false and
		jc.getDateFromString("20011232") = false and
		jc.getDateFromString("20011231").date2Str() = "20011231"
	;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT07:\tgetDateFromString";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT07

class CalendarT09 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar()
	in
	return
		jc.today().EQ(jc.getDateFrom_yyyy_mm_dd(2001, 3, 1)) and
		jc.readFromFiletoday(homedir ^ "/temp/BaseDay.txt").EQ(jc.getDateFrom_yyyy_mm_dd(2003, 10, 24))
	;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT09:\tRead today datefrom a file.";
protected tearDown: () ==> ()
tearDown() == return;

end CalendarT09

class CalendarT10 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar()
	in
	return
		jc.getLastDayOfMonth(2004, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 1, 31)) and
		jc.getLastDayOfMonth(2004, 2).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 29)) and
		jc.getLastDayOfMonth(2004, 3).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 3, 31)) and
		jc.getLastDayOfMonth(2004, 4).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 4, 30)) and
		jc.getLastDayOfMonth(2004, 5).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 5, 31)) and
		jc.getLastDayOfMonth(2004, 6).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 6, 30)) and
		jc.getLastDayOfMonth(2004, 7).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 7, 31)) and
		jc.getLastDayOfMonth(2004, 8).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 8, 31)) and
		jc.getLastDayOfMonth(2004, 9).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 9, 30)) and
		jc.getLastDayOfMonth(2004, 10).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 10, 31)) and
		jc.getLastDayOfMonth(2004, 11).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 11, 30)) and
		jc.getLastDayOfMonth(2004, 12).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 12, 31)) and
		jc.getLastDayOfMonth(2003, 13).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 1, 31)) and
		jc.getLastDayOfMonth(2003, 8+6).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 29)) and
		jc.getLastDayOfMonth(2003, 15).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 3, 31)) and
		jc.getLastDayOfMonth(2003, 16).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 4, 30)) and
		jc.getLastDayOfMonth(2003, 17).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 5, 31)) and
		jc.getLastDayOfMonth(2003, 18).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 6, 30)) and
		jc.getLastDayOfMonth(2003, 19).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 7, 31)) and
		jc.getLastDayOfMonth(2003, 20).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 8, 31)) and
		jc.getLastDayOfMonth(2003, 21).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 9, 30)) and
		jc.getLastDayOfMonth(2003, 22).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 10, 31)) and
		jc.getLastDayOfMonth(2003, 23).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 11, 30)) and
		jc.getLastDayOfMonth(2003, 24).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 12, 31)) and
		jc.getLastDayOfMonth(2005, 2).EQ(jc.getDateFrom_yyyy_mm_dd(2005, 2, 28))
	;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT10:\tGet the end of month.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT10

class CalendarT11 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar()
	in
	return
		jc.getRegularDate(2004, 1, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 1, 1)) and
		jc.getRegularDate(2003, 12, 32).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 1, 1)) and
		jc.getRegularDate(2003, 24, 32).EQ(jc.getDateFrom_yyyy_mm_dd(2005, 1, 1)) and
		jc.getRegularDate(2003, 13, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 1, 1)) and
		jc.getRegularDate(2004, 1, 32).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 1)) and
		jc.getRegularDate(2004, 2, 0).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 1, 31)) and
		jc.getRegularDate(2004, 2, 28).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 28)) and
		jc.getRegularDate(2004, 2, 29).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 29)) and
		jc.getRegularDate(2004, 3, 0).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 29)) and
		jc.getRegularDate(2004, 3, -1).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 28)) and
		jc.getRegularDate(2003, 2, 29).EQ(jc.getDateFrom_yyyy_mm_dd(2003, 3, 1)) and
		jc.getRegularDate(2004, 4, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 4, 1)) and
		jc.getRegularDate(2004, 0, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2003, 12, 1)) and
		jc.getRegularDate(2004, -1, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2003, 11, 1)) and
		jc.getRegularDate(2004, -10, 29).EQ(jc.getDateFrom_yyyy_mm_dd(2003, 3, 1)) and
		jc.getRegularDate(2004, -10, 28).EQ(jc.getDateFrom_yyyy_mm_dd(2003, 2, 28)) and
		jc.getRegularDate(2004, -11, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2003, 1, 1)) and
		jc.getRegularDate(2004, -12, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2002, 12, 1))
	;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT11:\tgetRegularDate";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT11

class CalendarT12 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar()
	in
	return
		jc.getRegularMonth(2004, 1) = mk_(2004, 1) and
		jc.getRegularMonth(2004, 2) = mk_(2004, 2) and
		jc.getRegularMonth(2004, 3) = mk_(2004, 3) and
		jc.getRegularMonth(2004, 4) = mk_(2004, 4) and
		jc.getRegularMonth(2004, 5) = mk_(2004, 5) and
		jc.getRegularMonth(2004, 6) = mk_(2004, 6) and
		jc.getRegularMonth(2004, 7) = mk_(2004, 7) and
		jc.getRegularMonth(2004, 8) = mk_(2004, 8) and
		jc.getRegularMonth(2004, 9) = mk_(2004, 9) and
		jc.getRegularMonth(2004, 10) = mk_(2004, 10) and
		jc.getRegularMonth(2004, 11) = mk_(2004, 11) and
		jc.getRegularMonth(2004, 12) = mk_(2004, 12) and
		jc.getRegularMonth(2004, 13) = mk_(2005, 1)  and
		jc.getRegularMonth(2004, 14) = mk_(2005, 2) and
		jc.getRegularMonth(2004, 24) = mk_(2005, 12) and
		jc.getRegularMonth(2004, 25) = mk_(2006, 1) and
		jc.getRegularMonth(2004, 0) = mk_(2003, 12) and
		jc.getRegularMonth(2004, -1) = mk_(2003, 11) and
		jc.getRegularMonth(2004, -10) = mk_(2003, 2) and
		jc.getRegularMonth(2004, -11) = mk_(2003, 1) and
		jc.getRegularMonth(2004, -12) = mk_(2002, 12) and
		jc.getRegularMonth(2004, -13) = mk_(2002, 11)
	;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT12:\tgetRegularMonth";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT12

JapaneseCalendar.vdmpp

class JapaneseCalendar is subclass of Calendar 
/*
Responsibility
	I'm a Japanese Calendar based on JST.
	Especially, I know Japanese holidays
*/

values
public differenceBetweenGMTandJST = 0.375;	-- 0.375 = 9 hours = 9 / 24 day
public differenceBetweenADandJapaneseCal = 1988;

functions

static private toStringAux: int -> seq of char
toStringAux(i) == 
	let	str = Integer`asString	in
	if i >= 10 then str(i) else " " ^ str(i);
	
static public getJapaneseDateStr : Date -> seq of char
getJapaneseDateStr(ADdate) == 
	let	asString =Integer`asString,
		yearOfJapaneseCal = ADdate.Year() - differenceBetweenADandJapaneseCal,
		m = ADdate.Month(),
		d = ADdate.day(),
		yearStr = asString(yearOfJapaneseCal),
		monthStr = toStringAux(m),
		dateStr = toStringAux(d)	in
		yearStr ^ monthStr ^ dateStr
pre
	ADdate.Year() >= differenceBetweenADandJapaneseCal;

operations

public setTheSetOfDayOffs: int ==> ()
setTheSetOfDayOffs(year) ==
	let	comingOfAgeDay = getNthDayOfTheWeek(year,1,2,<Mon>),
		marineDay = if year >= 2003 then getNthDayOfTheWeek(year,7, 3,<Mon>) else getDateFrom_yyyy_mm_dd(year,7,20),
		respect4TheAgedDay = if year >= 2003 then getNthDayOfTheWeek(year,9, 3,<Mon>) else getDateFrom_yyyy_mm_dd(year,9,15),
		healthSportsDay = getNthDayOfTheWeek(year,10, 2,<Mon>),
		nationalHolidaySet =  {
			getDateFrom_yyyy_mm_dd(year,1,1), 
			comingOfAgeDay,
			getDateFrom_yyyy_mm_dd(year,2,11),
			getVernalEquinox(year), 
			getDateFrom_yyyy_mm_dd(year,4,29),
			getDateFrom_yyyy_mm_dd(year,5,3),
			getDateFrom_yyyy_mm_dd(year,5,4), 	--formally this date is not national holiday
			getDateFrom_yyyy_mm_dd(year,5,5),
			marineDay,
			respect4TheAgedDay,
			getAutumnalEquinox(year),
			healthSportsDay,
			getDateFrom_yyyy_mm_dd(year,11,3),
			getDateFrom_yyyy_mm_dd(year,11,23),
			getDateFrom_yyyy_mm_dd(year,12,23)
		},
		mondayMakeupHolidat = 
			if year >= 2007 then 
				{getNotNationalHolidaysInFuture(nationalHolidaySet, d) | d in set nationalHolidaySet & isSunday(d)}
			else
				 {d.plus(1) | d in set nationalHolidaySet & isSunday(d)},
		weekdayBetweenDayOff = 
			if year >= 2007 then
				getWeekdayBetweenDayOff(nationalHolidaySet) 
			else
				{}
	in
	Year2Holidays := Year2Holidays munion { year |-> nationalHolidaySet union mondayMakeupHolidat union weekdayBetweenDayOff}
pre
	year >= 2000;

public JapaneseCalendar : () ==> JapaneseCalendar
JapaneseCalendar() ==
	(
	setDifferenceWithGMT(differenceBetweenGMTandJST); 
	return self
	);

public getWeekdayBetweenDayOff : set of Date ==> set of Date
getWeekdayBetweenDayOff(aNationalHolidaySet) == (
	let 
		candidatesOfWeekdayBetweenDayOff = 
			dunion { {d.minus(1), d.plus(1)} | d in set aNationalHolidaySet &
				d.minus(1).Year() = d.Year() and d.plus(1).Year() = d.Year()},
		weekdayBetweenHoliday = 
			{ d | d in set candidatesOfWeekdayBetweenDayOff & 
				let yesterday : Date = d.minus(1), tomorrow : Date =  d.plus(1) in
				isInDateSet(yesterday, aNationalHolidaySet) and isInDateSet(tomorrow, aNationalHolidaySet)}
	in
	return weekdayBetweenHoliday
 );

functions
public getNotNationalHolidaysInFuture :set of Date * Date-> Date
getNotNationalHolidaysInFuture(aNationalHolidaySet, date) ==
	cases  isInDateSet(date, aNationalHolidaySet) :
		(true)	-> getNotNationalHolidaysInFuture(aNationalHolidaySet, date.plus( 1)),
		others	-> date
	end;

end JapaneseCalendar

QueueT.vdmpp

class QueueT is subclass of TestDriver
functions
public tests : () -> seq of TestCase
tests () == 
	[ new QueueT01()
	];
end QueueT

class QueueT01 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	q0 = Queue`empty[int](),
		q1 = Queue`enQueue[int](1, q0),
		q2 = Queue`enQueue[int](2, q1),
		q3 = Queue`enQueue[int](3, q2),
		h1 = Queue`top[int](q3),
		q4 = Queue`deQueue[int](q3),
		q5 = Queue`deQueue[int](q4),
		q6 = Queue`deQueue[int](q5),
		h2 =  Queue`top[int](q6),
		q7 = Queue`deQueue[int](q6)
	in
	return
		q0 = [] and
		q1 = [1] and
		q2 = [1,2] and
		q3 = [1,2,3] and
		h1 = 1 and
		q4 = [2,3] and
		q5 = [3] and
		q6 = [] and
		h2 = nil and
		q7 = [] and
		Queue`isEmpty[int](q7) and
		not Queue`isEmpty[int](q5) 
		
;
protected setUp: () ==> ()
setUp() == TestName := "QueueT01:\t Test Queue";
protected tearDown: () ==> ()
tearDown() == return;
end QueueT01

TermT.vdmpp

class TermT is subclass of TestDriver 
functions
public tests : () -> seq of TestCase
tests() == 
	[ 
	new TermT01()
	];
end TermT
----------------------------------------------------------

class TermT01 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	cal = new JapaneseCalendar(),
		astartTime = new Time(cal, 2003, 7, 30, 14, 29, 30, 20),
		aendTime = new Time(cal, 2003, 7, 30, 14, 29, 30, 22),
		t1        = new Time(cal, 2003, 7, 30, 14, 29, 30, 19),
		t2        = new Time(cal, 2003, 7, 30, 14, 29, 30, 20),
		t3        = new Time(cal, 2003, 7, 30, 14, 29, 30, 21),
		t4        = new Time(cal, 2003, 7, 30, 14, 29, 30, 22),
		t5        = new Time(cal, 2003, 7, 30, 14, 29, 30, 23),
		t6        = new Time(cal, 2003, 7, 29, 14, 29, 30, 20),
		t7        = new Time(cal, 2003, 7, 31, 14, 29, 30, 20),
		t8        = new Time(cal, 2003, 7, 29, 14, 29, 29, 20),
		t9        = new Time(cal, 2003, 7, 29, 14, 29, 31, 20),
		term1 = new Term(astartTime, aendTime)
	in
	return
		not term1.isInThePeriod(t1, term1) and
		term1.isInThePeriod(t2, term1) and
		term1.isInThePeriod(t3, term1) and
		term1.isInThePeriod(t4, term1) and
		not term1.isInThePeriod(t5, term1) and
		not term1.isInThePeriod(t6, term1) and
		not term1.isInThePeriod(t7, term1) and
		not term1.isInThePeriod(t8, term1) and
		not term1.isInThePeriod(t9, term1)
	;
protected setUp: () ==> ()
setUp() == TestName := "TermT01:\tTest of term constructor and isInThePeriod()";
protected tearDown: () ==> ()
tearDown() == return;
end TermT01
----------------------------------------------------------

FunctionT.vdmpp

class FunctionT is subclass of TestDriver 
functions
public tests : () -> seq of TestCase
tests() == 
	[ 
	new FunctionT01(), new FunctionT02(),  new FunctionT03()
	];
end FunctionT
----------------------------------------------------------

class FunctionT01 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	f1 = lambda x : int & x * 2,
		p1 = lambda x : int & x > 1000,
		p11 = lambda x : int & x <= 1000,
		f2 = lambda x : seq of char & x ^ "0",
		p2 = lambda x : seq of char & len x > 9,
		p21 = lambda x : seq of char & len x <= 9
	in
	return
		Function`Fwhile[int](p11)(f1)(1) = 1024 and
		Function`Fwhile[seq of char](p21)(f2)("123456") = "1234560000" and
		Function`Funtil[int](p1)(f1)(1) = 1024 and
		Function`Funtil[seq of char](p2)(f2)("123456") = "1234560000"
	;
protected setUp: () ==> ()
setUp() == TestName := "FunctionT01:\tTest Fwhile, Funtil.";
protected tearDown: () ==> ()
tearDown() == return;
end FunctionT01
----------------------------------------------------------

class FunctionT02 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	f1 = lambda x : int & x * 2,
		f2 = lambda x : int & x * 3,
		f3 = lambda x : int & x ** 2,
		funcSeq1 = [f1, f2, f3],
		f10 = lambda x : seq of char & x ^ x,
		f11 = Sequence`take[char](10),
		f12 = Sequence`drop[char](4),
		funcSeq2 = [f10, f11, f12]
	in
	return
		Function`Seq[int](funcSeq1)(2) = (2 * 2 * 3) ** 2 and
		Function`Seq[seq of char](funcSeq2)("12345678") = "567812"
	;
protected setUp: () ==> ()
setUp() == TestName := "FunctionT02:\tTest function apply.";
protected tearDown: () ==> ()
tearDown() == return;
end FunctionT02
----------------------------------------------------------

class FunctionT03 is subclass of TestCase
types
public INT = int;
public ReadingFunctionType = INT -> INT -> INT;
--public ReadingFunctionType = int -> int -> int;

functions
public ReadingFunction: () -> ReadingFunctionType
ReadingFunction() == 
	let fn =  "./fread-func.txt"
	in
	Function`readFn[ReadingFunctionType](fn);

operations 
protected test: () ==> bool
test() == 
	return 
		ReadingFunction() (3)(2) = 1 and
		ReadingFunction() (4)(4) = 0 and
		ReadingFunction() (4)(-3) = -2 and
		ReadingFunction() (-4)(3) = 2
	;
protected setUp: () ==> ()
setUp() == TestName := "FunctionT03:\tTest of reading function.";
protected tearDown: () ==> ()
tearDown() == return;
end FunctionT03

FTestLogger.vdmpp

                                                                                                  
--$Id: TestLogger.vpp,v 1.1 2005/10/31 02:09:59 vdmtools Exp $
class FTestLogger
values
historyFileName =  "VDMTESTLOG.TXT";

functions
                                                                                                                                        
static public Success: FTestDriver`TestCase +> bool
Success(t) == 
	let	message = 
			FTestDriver`GetTestName(t)^"\tOK.\n",
		- = Fprint( message),
		- = Print(message)		
	in
	true;
                                                                                                                                         
static public Failure: FTestDriver`TestCase +> bool
Failure(t) == 
	let	message = FTestDriver`GetTestName(t)^"\tNG.\n",
		- = Fprint( message),
		- = Print( message)		
	in
	false;
                                                                                                                                                 
static public SuccessAll : seq of char +> bool
SuccessAll(m) ==
	let	message = m ^ "\tOK!!\n",
		- = Fprint(message),
		- = Print( message)
	in
	true;
                                                                                                                                                  	
static public FailureAll :  seq of char +> bool
FailureAll(m) ==
	let	message = m ^ "\tNG!!\n",
		- = Fprint( message),
		- = Print( message)
	in
	false;
                                                                                      
static public Print : seq of char -> bool
Print (s) == new IO().echo(s);
                                                                                                                                                 
static public Fprint : seq of char -> bool
Fprint (s) == new IO().fecho(historyFileName,  s, <append>);

operations
                                                                                                       
static public Pr : seq of char ==> ()
Pr (s) == let - = new IO().echo(s) in skip;
                                                                                                                                                                   
static public Fpr : seq of char ==> ()
Fpr (s) == let - = new IO().fecho(historyFileName,  s, <append>) in skip;

end FTestLogger
                                                                            

RealT.vdmpp

class RealT is subclass of TestDriver 
functions
public tests : () -> seq of TestCase
tests () == 
	[ 
	new RealT01(), new RealT02(), new RealT03(), new RealT04(),
	new RealT05(), new RealT06(), new RealT07(), new RealT08()
	];
end RealT
-----------------------------------------------------

class RealT01 is subclass of TestCase
values
	Tolelance = 1E-10;
operations 
protected test: () ==> bool
test() == 
	let	r = new Real()		in
	return
		Real`EQ(r.getInterest(2,10))(0.07177346254161253 )
;
protected setUp: () ==> ()
setUp() == TestName := "RealT01:\tTest of getInterest";
protected tearDown: () ==> ()
tearDown() == return;
end RealT01
-----------------------------------------------------

class RealT02 is subclass of TestCase
values
	Tolelance = 1E-10;
operations 
protected test: () ==> bool
test() == 
	let	r = new Real()		in
	return
		Real`EQ(r.root(2))(1.414213562382246 )
;
protected setUp: () ==> ()
setUp() == TestName := "RealT02:\tTest of root.";
protected tearDown: () ==> ()
tearDown() == return;
end RealT02
-----------------------------------------------------

class RealT03 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	r = new Real()		in
	return
		r.isNDigitsAfterTheDecimalPoint(10.01,2)  and
		not r.isNDigitsAfterTheDecimalPoint(10.01,3)  and
		r.isNDigitsAfterTheDecimalPoint(10.012,3)  and
		r.isNDigitsAfterTheDecimalPoint(10.0,0)  and
		r.isNDigitsAfterTheDecimalPoint(10.011,2) = false  and
		r.isNDigitsAfterTheDecimalPoint(10.1,0) = false and
		r.getNumberOfDigitsAfterTheDecimalPoint(-1.2) = 1 and
		r.getNumberOfDigitsAfterTheDecimalPoint(1.0) = 0 and
		r.getNumberOfDigitsAfterTheDecimalPoint(1) = 0 and
		r.getNumberOfDigitsAfterTheDecimalPoint(1.23) = 2
;
protected setUp: () ==> ()
setUp() == TestName := "RealT03:\tTest isNDigitsAfterTheDecimalPoint and getNumberOfDigitsAfterTheDecimalPoint.";
protected tearDown: () ==> ()
tearDown() == return;
end RealT03
-----------------------------------------------------

class RealT04 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	r = new Real()		in
	return
		r.numberOfDigit(0) = 1 and
		r.numberOfDigit(1) = 1 and
		r.numberOfDigit(9) = 1 and
		r.numberOfDigit(10) = 2 and
		r.numberOfDigit(99) = 2 and
		r.numberOfDigit(100) = 3 and
		r.numberOfDigit(0.1) = 3 and
		r.numberOfDigit(9.1) = 3 and
		r.numberOfDigit(10.1) = 4 and
		r.numberOfDigit(10.123) = 6
;
protected setUp: () ==> ()
setUp() == TestName := "RealT04:\tTest numberOfDigit.";
protected tearDown: () ==> ()
tearDown() == return;
end RealT04
-----------------------------------------------------

class RealT05 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	return
		Real`EQ(Real`roundAterDecimalPointByNdigit(10.12345, 4))( 10.1235) and
		Real`EQ(Real`roundAterDecimalPointByNdigit(10.12345, 3))( 10.123 ) and
		Real`EQ(Real`roundAterDecimalPointByNdigit(10.12345, 2))( 10.12)  and
		Real`EQ(Real`roundAterDecimalPointByNdigit(10.125, 2) )( 10.13)  and
		Real`EQ(Real`roundAterDecimalPointByNdigit(10.14, 1))(  10.1)  and
		Real`EQ(Real`roundAterDecimalPointByNdigit(10.15, 1) )(  10.2)  and
		Real`EQ(Real`roundAterDecimalPointByNdigit(10.5, 0))( 11)  and
		Real`EQ(Real`roundAterDecimalPointByNdigit(10.4, 0) )( 10)  
;
protected setUp: () ==> ()
setUp() == TestName := "RealT05:\tTest roundAterDecimalPointByNdigit.";
protected tearDown: () ==> ()
tearDown() == return;
end RealT05
-----------------------------------------------------

class RealT06 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	return
		Real`EQ(10.0123456678)(10.0123456789) = false and
		Real`EQ(10.01234567891)(10.01234567892) and
		Real`EQ(10.012345678801)(10.0123456789) and
		Real`EQE(1E-2)(10.12345)(10.12987)
;
protected setUp: () ==> ()
setUp() == TestName := "RealT06:\tTest EQ (Equal).";
protected tearDown: () ==> ()
tearDown() == return;
end RealT06
-----------------------------------------------------

class RealT07 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let f1 = lambda x : real & x ** 2
	in
	return
		Real`EQ(Real`integrate(f1)(10)(1)(2))(2.735) and
		Real`EQ(Real`integrate(f1)(100)(1)(2))(2.37335) and
		Real`EQ(Real`integrate(f1)(1000)(1)(2))(2.3373335)
;
protected setUp: () ==> ()
setUp() == TestName := "RealT07:\tTest integrate(x ** 2)";
protected tearDown: () ==> ()
tearDown() == return;
end RealT07
-----------------------------------------------------

class RealT08 is subclass of TestCase
values
pi = MATH`pi;
sin = MATH`sin

operations 
protected test: () ==> bool
test() == 
	return
		Real`EQ(Real`integrate(sin)(2)(0)(pi))(1.5707963278)  and 
		Real`EQ(Real`integrate(sin)(3)(0)(pi))(1.8137993649)  and 
		Real`EQ(Real`integrate(sin)(4)(0)(pi))(1.8961188984)  and 
		Real`EQ(Real`integrate(sin)(5)(0)(pi))(1.9337655984)  and
		Real`EQ(Real`integrate(sin)(2000)(1)(pi))(1.5403021586) 
;
protected setUp: () ==> ()
setUp() == TestName := "RealT08:\tTest integrate(sin) .";
protected tearDown: () ==> ()
tearDown() == return;
end RealT08




TestCase.vdmpp

class TestCase

instance variables

	public TestName: seq of char := "** anonymous regression test **";

operations
public TestACase: () ==> bool
TestACase() == 
	(dcl	r: bool;
	setUp();
	r := test();
	tearDown();
	return r);
	
public getTestName: () ==> seq of char
getTestName() == return TestName;

protected test: () ==> bool
test() == is subclass responsibility;

protected setUp: () ==> ()
setUp() == return;

protected tearDown: () ==> ()
tearDown() == return;

end TestCase

Date.vdmpp

class Date  is subclass of CalendarDefinition	-- date
/*
Responsibility
	I am a date of Gregorio Calendar.
Abstract
	I calculate date by cooperating with Calendar class.
	There can be two or more objects at the same date. 

Therefore, it is judged that the date is equal by using EQ operation. 
*/

instance variables

private ModifiedJulianDate : real := 0;
private usingCalendar : Calendar;

/*
ModifiedJulianDateは、julianDateでは数値が大きくなりすぎたので採用されたdateを表す数値で、1858年11月17日を0とする。
calculation誤差の関係から、2倍精度浮動小数点(Cではdouble)でなければならない。
*/

functions

----Query

public getNumberOfDayOfTheWeek: () -> Calendar`NumberOfDayOfTheWeek
getNumberOfDayOfTheWeek() == calendar().getNumberOfDayOfTheWeek(self);

public getNameOfDayOfTheWeek : () -> Calendar`NameOfDayOfTheWeek
getNameOfDayOfTheWeek() == calendar().getNameOfDayOfTheWeek(self) ;

--指定された曜日が、selfとdateの間に何日あるかを返す。 
public getNumberOfTheDayOfWeek: Date * Calendar`NameOfDayOfTheWeek -> int
getNumberOfTheDayOfWeek(date,nameOfDayOfTheWeek) == calendar().getNumberOfTheDayOfWeek(self,date,nameOfDayOfTheWeek);

--selfとdateの間の休日あるいは日曜日の数を返す(startDateを含む)
public getTheNumberOfDayOff: Date -> int
getTheNumberOfDayOff(date) == calendar().getTheNumberOfDayOff(self,date);

--selfとdateの間の休日あるいは日曜日の数を返す(startDateを含まない)
public getTheNumberOfDayOffExceptStartDate: Date -> int
getTheNumberOfDayOffExceptStartDate(date) == calendar().getTheNumberOfDayOffExceptStartDate(self,date) ;

--dateから、そのdateの属する年を求める。
public Year: () -> int
Year() == calendar().Year(self);
		
--dateから、そのdateの属する月を求める。
public Month: () -> int
Month() == calendar().Month(self);
		
--dateから、日を求める。
public day: () -> int
day() == calendar().day(self);

/* calculation  */

--休日でないdateを返す(未来へ向かって探索する)
public getFutureWeekday : ()-> Date
getFutureWeekday() == calendar().getFutureWeekday(self);

--休日でないdateを返す(過去へ向かって探索する)
public getPastWeekday : ()-> Date
getPastWeekday() == calendar().getPastWeekday(self);

--selfに、平日n日分を加算する
public addWeekday : int -> Date
addWeekday(addNumOfDays) == calendar().addWeekday(self,addNumOfDays);

--selfに、平日n日分を減算する
public subtractWeekday : int -> Date
subtractWeekday(subtractNumOfDays) == calendar().subtractWeekday(self,subtractNumOfDays) ;

/* checking */

public isSunday : () -> bool
isSunday() == calendar().isSunday(self);

public isSaturday : () -> bool
isSaturday() == calendar().isSaturday(self);

public isWeekday : () -> bool
isWeekday() == calendar().isWeekday(self);

public isNotDayOff : () -> bool
isNotDayOff() == calendar().isNotDayOff(self);

public isDayOff : () -> bool 
isDayOff() == calendar().isDayOff(self);

public isSundayOrDayoff : () -> bool 
isSundayOrDayoff() ==  calendar().isSundayOrDayoff(self);

--new Date().getDateFrom_yyyy_mm_dd(2001,12,31).daysFromNewYear() = 365
public daysFromNewYear: () -> int
daysFromNewYear() == calendar().daysFromNewYear(self);

/* conversion */

public get_yyyy_mm_dd: () -> int * int * int
get_yyyy_mm_dd() == mk_(self.Year(), self.Month(), self.day());

private toStringAux: int -> seq of char
toStringAux(i) == 
	let	str = Integer`asString	in
	if i >= 10 then str(i) else "0" ^ str(i);

public date2Str: () -> seq of char
date2Str() == self.asString();

operations

----conversion

public asString: () ==> seq of char
asString() ==
	(let	asString =Integer`asString,
		y = self.Year(),
		m = self.Month(),
		d = self.day(),
		yearStr = asString(y),
		monthStr = toStringAux(m),
		dateStr = toStringAux(d)
	in
		return yearStr ^ monthStr ^ dateStr
	);

public print: ()   ==> seq of char
print() ==
	(let	asString =Integer`asString,
		y = self.Year(),
		m = self.Month(),
		d = self.day(),
		yearStr = asString(y),
		monthStr = toStringAux(m),
		dateStr = toStringAux(d)
	in
		return "Year=" ^ yearStr ^ ", Month=" ^ monthStr ^ ", Day=" ^ dateStr ^ ", "
	);


----比較

/*
操作名
	大小比較を行う関数群。
引数
	date
返値
	真ならtrueを返し、そうでなければfalseを返す。
内容
	自身と与えられたdateの大小比較を行う。
*/
public LT: Date ==> bool
LT(date) == return floor self.getModifiedJulianDate() < floor date.getModifiedJulianDate();

public GT: Date ==> bool
GT(date) == return floor self.getModifiedJulianDate() > floor date.getModifiedJulianDate();

public LE: Date ==> bool
LE(date) == return not self.GT(date);

public GE: Date ==> bool
GE(date) == return not self.LT(date);

--自身と与えられたdateがEQか判定する。
public EQ: Date ==> bool	--等しければtrueを返し、そうでなければfalseを返す。
EQ(date) ==  return (floor self.getModifiedJulianDate() = floor date.getModifiedJulianDate());

--自身と与えられたdateが等しくないか判定する。
public NE: Date ==> bool	--等しければfalseを返し、そうでなければtrueを返す。
NE(date) ==  return (floor self.getModifiedJulianDate() <> floor date.getModifiedJulianDate());

----calculation

--自身にnumOfDaysを加算したdateを返す
public plus: int ==> Date
plus(addNumOfDays) == return calendar().modifiedJulianDate2Date(self.getModifiedJulianDate() + addNumOfDays) ;

--自身からnumOfDaysを減算したdateを返す
public minus: int ==> Date
minus(subtractNumOfDays) == return calendar().modifiedJulianDate2Date(self.getModifiedJulianDate() - subtractNumOfDays) ;

--インスタンス変数へのアクセス操作

--ModifiedJulianDate
public setModifiedJulianDate: real ==> ()
setModifiedJulianDate(r) == ModifiedJulianDate := r;

public getModifiedJulianDate: () ==> real
getModifiedJulianDate() == return ModifiedJulianDate;

public calendar : () ==> Calendar
calendar() == return usingCalendar;

--Constructor
public Date : Calendar * real ==> Date
Date(aCal, aModifiedJulianDate) == 
	(
	usingCalendar := aCal;
	setModifiedJulianDate(aModifiedJulianDate);
	return self
	);

end Date

Product.vdmpp

class Product 

functions

static public Curry[@T1, @T2, @T3] : (@T1 * @T2 -> @T3) -> @T1 -> @T2 -> @T3
Curry(f)(x)(y) == f(x, y);

static public Uncurry[@T1, @T2, @T3] : (@T1 -> @T2 -> @T3) -> @T1 * @T2 -> @T3
Uncurry(f)(x,y) == f(x)(y);

end Product

FHashtable.vdmpp

                                                                                           
--"$Id"
class FHashtable

functions
                                                                                             
static public Put[@T1, @T2] : 
	(map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> @T1 -> @T2 
	-> (map @T1 to (map @T1 to  @T2))
Put(aHashtable)(aHashCode)(aKey)(aValue) ==
	let	hashcode = aHashCode(aKey)
	in
	if hashcode in set dom aHashtable then
		aHashtable ++ {hashcode |-> (aHashtable(hashcode) ++ {aKey |-> aValue})}
	else
		aHashtable munion {hashcode |-> {aKey |-> aValue}}
	;
                                                                                            
static public PutAll[@T1, @T2] : 
	(map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> (map @T1 to  @T2) 
	-> (map @T1 to (map @T1 to  @T2)) 
PutAll(aHashtable)(aHashCode)(aMap) == 
	PutAllAux[@T1, @T2](aHashtable)(aHashCode)(aMap)(dom aMap);

static public PutAllAux[@T1, @T2] :
	(map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> (map @T1 to  @T2)  -> set of @T1
	-> (map @T1 to (map @T1 to  @T2)) 
PutAllAux(aHashtable)(aHashCode)(aMap)(aKeySet) ==
	if aKeySet = {} then
		aHashtable
	else
		let	aKey in set aKeySet	in
		let	newHashtable = Put[@T1, @T2](aHashtable)(aHashCode)(aKey)(aMap(aKey))	
		in
		PutAllAux[@T1, @T2](newHashtable)(aHashCode)(aMap)(aKeySet \ {aKey})
	;
                                                                              
static public Get[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> @T1  -> [@T2]
Get(aHashtable)(aHashCode)(aKey) ==
	let	hashcode = aHashCode(aKey)
	in
	if hashcode in set dom aHashtable then
		FMap`Get[@T1, @T2](aHashtable(hashcode))(aKey)
	else
		nil
	;
                                                                                                              
static public Remove[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> @T1 -> (map @T1 to (map @T1 to  @T2))
Remove(aHashtable)(aHashCode)(aKey) == 
	let	hashcode = aHashCode(aKey)
	in
	{h |-> ({aKey} <-: aHashtable(hashcode)) | h in set {hashcode}} munion 
		{hashcode} <-: aHashtable ;
                                                                               
static public Clear[@T1, @T2] : () -> (map @T1 to (map @T1 to  @T2))
Clear() == ({ |-> });
                                                                                               
static public KeySet[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> set of  @T1
KeySet(aHashtable) == 
	--let	aMapSet : set of (map @T1 to @T2) = rng aHashtable,
		--f : map @T1 to @T2 -> set of @T1 = lambda x : map @T1 to  @T2 & dom x
	let	aMapSet = rng aHashtable
	in
	if aMapSet <> {} then
		--dunion FSet`Fmap[map @T1 to  @T2, set of @T1](f)(aMapSet)
		dunion  {dom s | s in set aMapSet} 
	else
		{};
                                                                                           
static public ValueSet[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> set of  @T2
ValueSet(aHashtable) == 
	--let	aMapSet : set of (map @T1 to @T2) = rng aHashtable,
		--f : map @T1 to @T2 -> set of @T2 = lambda x : map @T1 to  @T2 & rng x
	let	aMapSet = rng aHashtable
	in
	if aMapSet <> {} then
		--dunion FSet`Fmap[map @T1 to  @T2, set of @T2](f)(aMapSet)
		dunion  {rng s | s in set aMapSet} 
	else
		{};
                                                                            
static public Size[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> nat
Size(aHashtable) == card KeySet[@T1, @T2](aHashtable) ;
                                                                                          
static public IsEmpty[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> bool
IsEmpty(aHashtable) == KeySet[@T1, @T2](aHashtable) = {};
                                                                                                       
static public Contains[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> @T2 -> bool
Contains(aHashtable)(aValue) == 
	let	aMapSet = rng aHashtable	
	in
	if aMapSet <> {} then
		exists aMap in set aMapSet & aValue in set rng aMap
	else
		false;
                                                                                                               
static public ContainsKey[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> @T1 -> bool
ContainsKey(aHashtable)(aKey) == 
	let	aMapSet = rng aHashtable	
	in
	if aMapSet <> {} then
		exists aMap in set aMapSet & aKey in set dom aMap
	else
		false;

end FHashtable
                                                                           

FTestDriver.vdmpp

                                                                                                                                                
--$Id: TestDriver.vpp,v 1.1 2005/10/31 02:09:59 vdmtools Exp $
class FTestDriver

types
public TestCase ::
	testCaseName : seq of char
	testResult : bool;

functions
                                                                                                                                                                                                                                                          
static public run: seq of FTestDriver`TestCase +> bool
run(t) ==
	let	m = "Result-of-testcases.",
		r = [isOK(t(i)) | i in set inds t]
	in
	if  forall i in set inds r & r(i) then
		FTestLogger`SuccessAll(m)
	else
		FTestLogger`FailureAll(m);
                                                                                                                                                                                                               
static public isOK: FTestDriver`TestCase +> bool
isOK(t) ==
	if GetTestResult(t) then
		FTestLogger`Success(t)
	else
		FTestLogger`Failure(t);
                                                                           
static public GetTestResult : FTestDriver`TestCase +> bool
GetTestResult(t) == t.testResult;
                                                                       	
static public GetTestName: FTestDriver`TestCase +> seq of char
GetTestName(t) == t.testCaseName;

end FTestDriver

                                                                             

IntegerT.vdmpp

class IntegerT is subclass of TestDriver
functions
public tests : () -> seq of TestCase
tests () == 
	[ new IntegerT01(), new IntegerT02()
	];
end IntegerT
---------------------------------------
class IntegerT01 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	i = new Integer()		in
	return
		(i.asString(1234567890) = "1234567890" and
		i.asString(-1234567890) = "-1234567890" and
		i.asStringZ("zzz9")(9900) = "9900" and
		i.asStringZ("9")(0) = "0" and
		i.asStringZ("z")(0) = " " and
		i.asStringZ("z")(9) = "9" and
		i.asStringZ("zzz9")(9) = "   9" and
		i.asStringZ("0009")(9) = "0009" and
		i.asStringZ("-0009")(9) = "0009" and
		i.asStringZ("-zzz9")(-9999) = "-9999" and
		i.asStringZ("-zzz9")(-9) = "-   9" and
		i.asStringZ("zzz9")(-9999) = "9999" and
		i.asStringZ("zzz9")(-9) = "   9" and
		i.asString(0) = "0" and
		i.asChar(0) = "0" and 
		i.asChar(1) = "1" and
		i.asChar(2) = "2" and
		i.asChar(3) = "3" and
		i.asChar(4) = "4" and 
		i.asChar(5) = "5" and 
		i.asChar(6) = "6" and
		i.asChar(7) = "7" and
		i.asChar(8) = "8" and
		i.asChar(9) = "9" and
		i.asChar(10) = false
		)
;
protected setUp: () ==> ()
setUp() == TestName := "IntegerT01:\tConvert integer to string.";
protected tearDown: () ==> ()
tearDown() == return;
end IntegerT01
---------------------------------------

class IntegerT02 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	gcd = Integer`GCD(24),
		lcm = Integer`LCM(7)
	in
	return
		Sequence`fmap[nat, nat](gcd)([36, 48, 16]) = [12, 24, 8]  and
		Sequence`fmap[nat, nat](lcm)([3, 4, 5]) = [21, 28, 35]
;
protected setUp: () ==> ()
setUp() == TestName := "IntegerT02:\tGet GCD and LCM.";
protected tearDown: () ==> ()
tearDown() == return;
end IntegerT02

MapT.vdmpp

class MapT is subclass of TestDriver
functions
public tests : () -> seq of TestCase
tests() == 
	[ 
	new MapT01(), new MapT02()	
	];
end MapT
----------------------------------------------------
class MapT01 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	m1 = {1 |-> "Kei Sato", 19 |-> "Shin Sahara", 20 |-> "Hiroshi Sakoh"},
		m2 = {"Kei Sato" |-> 1,  "Shin Sahara" |-> 19,  "Hiroshi Sakoh" |-> 20},
		get1 = Map`Get[int, seq of char],
		get2 = Map`Get[seq of char, int]
	in
	return 
		get1(m1)(19) = "Shin Sahara" and
		get1(m1)(2) = nil and
		get2(m2)("Shin Sahara") = 19 and
		get2(m2)("Worst Prime Minister Koizumi") = nil
;
protected setUp: () ==> ()
setUp() == TestName := "MapT01:\tTest of Get function.";
protected tearDown: () ==> ()
tearDown() == return;
end MapT01
----------------------------------------------------
class MapT02 is subclass of TestCase, CommonDefinition
operations 
protected test: () ==> bool
test() == 
	let	m1 = {1 |-> "Kei Sato", 19 |-> "Shin Sahara", 20 |-> "Hiroshi Sakoh"},
		m2 = {"Kei Sato" |-> 1,  "Shin Sahara" |-> 19,  "Hiroshi Sakoh" |-> 20},
		c1 = Map`Contains[int, seq of char],
		k1 = Map`ContainsKey[int, seq of char],
		c2 = Map`Contains[seq of char, int],
		k2 = Map`ContainsKey[seq of char, int]
	in
	return 
		c1(m1)("Kei Sato") and c1(m1)("Shin Sahara") and c1(m1)("Hiroshi Sakoh") and
		c1(m1)("Worst Prime Minister Koizumi") = false and
		k1(m1)(1) and k1(m1)(19) and k1(m1)(20) and
		not k1(m1)(99) and
		c2(m2)(1) and c2(m2)(19) and c2(m2)(20) and
		c2(m2)(30) = false and
		k2(m2)("Kei Sato") and k2(m2)("Shin Sahara") and k2(m2)("Hiroshi Sakoh") and
		k2(m2)("Worst Prime Minister Koizumi") = false
;
protected setUp: () ==> ()
setUp() == TestName := "MapT02:\tTest of Contains related functions.";
protected tearDown: () ==> ()
tearDown() == return;
end MapT02

Time.vdmpp

class Time is subclass of CalendarDefinition
/*
Responsibility
	時間を表す。
Abstract
	私は時間あるいはアナリシス・パターンで言うところの時点であり、aDateの時間を表す。
	例えば2003年7月28日14時15分59秒を表す。
*/

values
public hoursPerDay = 24;	--1日の時間数
public minutesPerHour = 60;	--1時間の分数
public secondsPerMinute = 60;	--1分の秒数
public ミリ = 1000;		--ミリを通常の単位にするための倍数
public milliSecondsPerDay = hoursPerDay * minutesPerHour * secondsPerMinute * ミリ;	--1日=24時間をmilliSecondで表した数
public milliSecondsPerHour = minutesPerHour * secondsPerMinute * ミリ;	--1時間をmilliSecondで表した数
private io = new IO();

types
public TimeInMilliSeconds = nat;	--1日の時刻を0時を0としたmilliSecond単位で持つ。
	
instance variables
/* 本来は、Javaのようにdate・時間を合わせてmilliSecond単位で持つべきだろうが、
  Dateは倍精度浮動小数点数でModifiedJulianDateを持っているため、時間の精度は5分程度となる。
  このため、dateと時刻を分けて持つことにした。
*/
sDate : Date;
sTime : TimeInMilliSeconds;
	
operations
--Constructor
public Time : Calendar * int * int * int * nat * nat * nat  * nat ==> Time
Time(cal, year, month, 日, 時, aMinute, aSecond, milliSecond) ==
	(
	sDate := cal.getDateFrom_yyyy_mm_dd(year, month, 日);
	sTime := self.IntProduct2TimeMillieSeconds(時, aMinute, aSecond, milliSecond);
	return self
	);

public Time : Calendar * int * int * int ==> Time
Time(cal, year, month, 日) ==
	(
	sDate := cal.getDateFrom_yyyy_mm_dd(year, month, 日);
	sTime := self.IntProduct2TimeMillieSeconds(0, 0, 0, 0);
	return self
	);
	
public Time : Date ==> Time
Time(aDate) ==
	(
	sDate := aDate;
	sTime := self.IntProduct2TimeMillieSeconds(0, 0, 0, 0);
	return self
	);
	
--currentDateTimeを求める単体テスト用関数。
public Time: Calendar ==> Time
Time(cal) == 
	(
	let	currentDateTime = readCurrentDateTime(homedir ^ "/temp/Today.txt", homedir ^ "/temp/Now.txt", cal)
	in
	(
	sDate := currentDateTime.getDate();
	sTime := currentDateTime.getTime();
	);
	return self
	);


--currentDateTimeを指定したreadFromFile単体テスト用関数。
public Time: seq of char * seq of char * Calendar ==> Time
Time(dateFileName, 時間fname, cal) ==
	(
	let	currentDateTime = readCurrentDateTime(dateFileName, 時間fname, cal)
	in
	(
	sDate := currentDateTime.getDate();
	sTime := currentDateTime.getTime();
	);
	return self
	);
		
--currentDateTimeをreadFromFile
public readCurrentDateTime : seq of char * seq of char * Calendar ==> [Time]
readCurrentDateTime(dateFileName, 時間fname, cal) ==
	let	mk_(結果, mk_(h, m, s, ms)) = io.freadval[int * int * int * int](時間fname)
	in
	if 結果 then
		let	d = cal.readFromFiletoday(dateFileName)	in
		return new Time(cal, d.Year(),  d.Month(), d.day(), h, m, s, ms)
	else
		let	- = io.echo("Can't read Current Date-Time data file.")
		in
		return nil;

--インスタンス変数操作

public getDate : () ==> Date
getDate() == return sDate;	

public setDate : Date ==> ()
setDate(aDate) == sDate := aDate;

public getTime : () ==> TimeInMilliSeconds
getTime() == return sTime;

public setTime : TimeInMilliSeconds ==> ()
setTime(aTime) == sTime :=aTime;

public hour: () ==> nat
hour() == 
	let	mk_(hour, -, -, -) = self.Time2IntProduct(self.getTime())
	in
	return hour;

public setTimeFromNat : nat ==> ()
setTimeFromNat(aTime) ==
	let	mk_(-, aMinute, aSecond, milliSecond) = self.Time2IntProduct(self.getTime())
	in
	self.setTime(IntProduct2TimeMillieSeconds(aTime, aMinute, aSecond, milliSecond));
	
public minute: () ==> nat
minute() == 
	let	mk_(-, aMinute, -, -) = self.Time2IntProduct(self.getTime())
	in
	return aMinute;
	
public setMinuteFromNat : nat ==> ()
setMinuteFromNat(minute) ==
	let	mk_(hour, -, aSecond, milliSecond) = self.Time2IntProduct(self.getTime())
	in
	self.setTime(IntProduct2TimeMillieSeconds(hour, minute, aSecond, milliSecond));
		
public second: () ==> nat
second() ==
	let	mk_(-, -, aSecond, -) = self.Time2IntProduct(self.getTime())
	in
	return aSecond;
	
public setSecond : nat ==> ()
setSecond(aSecond) ==
	let	mk_(hour, aMinute, -, milliSecond) = self.Time2IntProduct(self.getTime())
	in
	self.setTime(IntProduct2TimeMillieSeconds(hour, aMinute, aSecond, milliSecond));
		
public milliSecond: () ==> nat
milliSecond() ==
	let	mk_(-, -, -, milliSecond) = self.Time2IntProduct(self.getTime())
	in
	return milliSecond;
	
public setMilliSecond : nat ==> ()
setMilliSecond(aMilliSecond) ==
	let	mk_(hour, aMinute, aSecond, -) = self.Time2IntProduct(self.getTime())
	in
	self.setTime(IntProduct2TimeMillieSeconds(hour, aMinute, aSecond, aMilliSecond));
	
functions
-- Get attribute.

--時間から、その時間の属する暦を求める。
public calendar : () -> Calendar
calendar() == getDate().calendar();

--時間から、その時間の属する年を求める。
public Year: () -> int
Year() == self.getDate().calendar().Year(self.getDate());
		
--時間から、その時間の属する月を求める。
public Month: () -> int
Month() == self.getDate().calendar().Month(self.getDate());
		
--時間から、日を求める。
public day: () -> int
day() == self.getDate().calendar().day(self.getDate());

public getTimeAsNat : () -> nat
getTimeAsNat() == self.getTime();

----Compare

public LT: Time -> bool
LT(aTime) == 
	let	date1 = floor self.getDate().getModifiedJulianDate(),
		date2 = floor aTime.getDate().getModifiedJulianDate()
	in
	cases true :
	(date1 < date2)	-> true,
	(date1 = date2)	-> 
		if self.getTimeAsNat() < aTime.getTimeAsNat() then
			true
		else
			false,
	others		-> false
	end;

public GT: Time -> bool
GT(aTime) == not (self.LT(aTime) or self.EQ(aTime));

public LE: Time -> bool
LE(aTime) == not self.GT(aTime);

public GE: Time -> bool
GE(aTime) == not self.LT(aTime);

--自身と与えられた時間がEQか判定する。
public EQ: Time  ->  bool
EQ(aTime) == 
	self.getDate().EQ(aTime.getDate()) and self.getTimeAsNat() = aTime.getTimeAsNat();

--自身と与えられた時間が等しくないか判定する。
public NE: Time ->  bool
NE(aTime) ==  not self.EQ(aTime);

--変換

public IntProduct2TimeMillieSeconds : int * int * int * int -> int
IntProduct2TimeMillieSeconds(hour, aMinute, aSecond, milliSecond) ==((hour * minutesPerHour + aMinute) * secondsPerMinute + aSecond) * ミリ + milliSecond;

public Time2IntProduct : TimeInMilliSeconds -> nat * nat * nat * nat
Time2IntProduct(aTime) ==
	let	hms = aTime div ミリ,
		milliSecond = aTime mod ミリ,
		hm = hms div secondsPerMinute,
		aSecond = hms mod secondsPerMinute,
		hour = hm div minutesPerHour,
		aMinute = hm mod minutesPerHour
	in
	mk_(hour, aMinute, aSecond, milliSecond);

operations
public asString : () ==> seq of char
asString() == 
	let	mk_(hour, aMinute, aSecond, milliSecond) = self.Time2IntProduct(self.getTime())
	in
	return 
		self.getDate().asString() ^ 
		Integer`asString(hour) ^
		Integer`asString(aMinute) ^
		Integer`asString(aSecond) ^
		Integer`asStringZ("009")(milliSecond);

public print : () ==> seq of char
print() == 
	let	mk_(hour, aMinute, aSecond, milliSecond) = self.Time2IntProduct(self.getTime())
	in
	return 
		self.getDate().print() ^ 
		Integer`asString(hour) ^ "Hour, " ^
		Integer`asString(aMinute) ^ "Minute, " ^
		Integer`asString(aSecond) ^ "Second, " ^
		Integer`asStringZ("009")(milliSecond) ^ "MilliSecond" ;

----calculation

--milliSecondを加算する
public plusmilliSecond : int ==> Time
plusmilliSecond(aMilliSecond) == 
	let	time = self.getTime() + aMilliSecond,
		CarriedNumOfDays = 
			if time >= 0 then
				time div milliSecondsPerDay
			else
				time div milliSecondsPerDay - 1,
		newTime = time mod milliSecondsPerDay
	in
	(
	dcl aTime : Time := new Time(self.calendar(), self.Year(), self.Month(), self.day()) ;
	aTime.setTime(newTime);
	aTime.setDate(aTime.getDate().plus(CarriedNumOfDays));
	return aTime
	);
	
public plussecond : int ==> Time
plussecond(aSecond) == self.plusmilliSecond(aSecond * ミリ);
	
public plusminute : int ==> Time
plusminute(minute) == self.plusmilliSecond(minute * secondsPerMinute * ミリ);
	
public plushour : int ==> Time
plushour(hour) == self.plusmilliSecond(hour * minutesPerHour * secondsPerMinute * ミリ);
	
public plus: int * int * int * int ==> Time
plus(hour, aMinute, aSecond, milliSecond) == self.plusmilliSecond(IntProduct2TimeMillieSeconds(hour, aMinute, aSecond, milliSecond));
	
--milliSecondを減算する
public minusmilliSecond : int ==> Time
minusmilliSecond(aMilliSecond) == return self.plusmilliSecond(-aMilliSecond);
		
public minus: int * int * int * int  ==> Time
minus(hour, aMinute, aSecond, milliSecond) == self.minusmilliSecond(IntProduct2TimeMillieSeconds(hour, aMinute, aSecond, milliSecond));
		
end Time

FMap.vdmpp

                                                                                  
--"$Id"
class FMap

functions
                                                                                                                                 
static public Get[@T1, @T2] : map @T1 to @T2 -> @T1 -> [@T2]
Get(aMap)(aKey) ==
	if aKey in set dom aMap then
		aMap(aKey)
	else
		nil;
                                                                                                                 
static public Contains[@T1, @T2] : map @T1 to @T2 -> @T2 -> bool
Contains(aMap)(aValue) == aValue in set rng aMap;
                                                                                                                     
static public ContainsKey[@T1, @T2] : map @T1 to @T2 -> @T1 -> bool
ContainsKey(aMap)(aKey) == aKey in set dom aMap;
	
end FMap
                                                              

String.vdmpp

class String is subclass of Sequence

functions

--Conversion functions
static public asInteger: seq of char -> int
asInteger(s) == String`AsIntegerAux(s)(0);

static private AsIntegerAux : seq of char -> int -> int
AsIntegerAux(s)(sum) ==
	if s = [] then
		sum
	else
		AsIntegerAux(tl s)(10 * sum + Character`asDigit(hd s));
--	measure length;

static length : seq of char +> nat
length(s) == len s;

static lengthNil : [seq of char] +> nat
lengthNil(s) == if s = nil then 0 else len s;
	
--Decision functions
static public isSomeString: (char -> bool) -> seq of char -> bool
isSomeString(f)(s) == forall i in set inds s & f(s(i));

static public isDigits : seq of char -> bool
isDigits(s) == isSomeString(Character`isDigit)(s);

static public isLetters : seq of char -> bool
isLetters(s) == isSomeString(Character`isLetter)(s);

static public isLetterOrDigits : seq of char -> bool
isLetterOrDigits(s) == isSomeString(Character`isLetterOrDigit)(s);

static public isSpaces : [seq of char] -> bool
isSpaces(s) ==isSomeString(lambda c : char & c = ' ' or c = '\t')(s);

static public LT : seq of char * seq of char -> bool
LT(s1, s2) == String`LT2(s1)(s2);

static public LT2 : seq of char -> seq of char -> bool
LT2(s1)(s2) == 
	cases mk_(s1,s2):
		mk_([],[])		-> false,
		mk_([],-)		-> true,
		mk_(-^-,[])	-> false,
		mk_([head1]^tails1,[head2]^tails2)	->
			if Character`LT(head1,head2) then
				true
			elseif Character`LT(head2,head1) then
				false
			else
				String`LT(tails1, tails2)
	end;

static public LE : seq of char * seq of char -> bool
LE(s1, s2) == String`LE2(s1)(s2);

static public LE2 : seq of char -> seq of char -> bool
LE2(s1)(s2) == String`LT2(s1)(s2) or s1 = s2;

static public GT : seq of char * seq of char -> bool
GT(s1, s2) == String`GT2(s1)(s2);

static public GT2 : seq of char -> seq of char -> bool
GT2(s1)(s2) == String`LT(s2, s1);

static public GE : seq of char * seq of char -> bool
GE(s1, s2) == String`GE2(s1)(s2);

static public GE2 : seq of char -> seq of char -> bool
GE2(s1)(s2) == not String`LT2(s1)(s2);

static public Index: char -> seq of char -> int
Index(c)(aStr) == Sequence`Index[char](c)(aStr);

static public indexAll : seq of char * char -> set of int
indexAll(aStr,c) == Sequence`IndexAll2[char](c)(aStr);

static public IndexAll2 : char -> seq of char -> set of int
IndexAll2(c)(aStr) == Sequence`IndexAll2[char](c)(aStr);

static public isInclude : seq of char -> seq of char -> bool
isInclude(aStr)(aTargetStr) ==
	let	indexSet = indexAll(aStr,aTargetStr(1))
	in	exists i in set indexSet & 
			SubStr(i)(len aTargetStr)(aStr) = aTargetStr
pre
	aTargetStr <> ""
	;

static public subStr :
	seq1 of char * nat * nat -> seq of char
subStr(aStr,fromPos,length) == aStr(fromPos,...,fromPos+length-1);

static public SubStr : nat -> nat -> seq1 of char -> seq of char
SubStr(fromPos)(length)(aStr) == aStr(fromPos,...,fromPos+length-1);

static public GetToken : seq of char * set of char -> seq of char
GetToken(s, aDelimitterSet) == 
	TakeWhile[char](lambda c : char & c not in set aDelimitterSet)(s);

static public DropToken : seq of char * set of char -> seq of char
DropToken(s, aDelimitterSet) == 
	DropWhile[char](lambda c : char & c not in set aDelimitterSet)(s);

static public getLines : seq of char -> seq of seq of char
getLines(s) ==
	getLinesAux(s)([]);

static public getLinesAux : seq of char -> seq of seq of char -> seq of seq of char
getLinesAux(s)(line) ==
	if s = [] then
		line
	else
		let wDelimitterSet = {'\n'},
			wHeadLine = GetToken(s, wDelimitterSet),
			wTailStringCandidate = DropToken(s, wDelimitterSet),
			wTailString = 
				if wTailStringCandidate <> [] and hd wTailStringCandidate = '\n' then tl wTailStringCandidate 
				else wTailStringCandidate
		in
		getLinesAux(wTailString)(line ^ [wHeadLine]);
--measure length;

operations
static public index: seq of char * char ==> int
index(aStr,c) == (
	for i = 1 to len aStr do
		if aStr(i) = c then return i;
	return 0
);

static public subStrFill :
	seq of char * nat * nat * char ==> seq of char
subStrFill(aStr,fromPos,length, fillChar) ==
	let	lastPos = fromPos+length-1
	in (
		dcl aResult : seq of char := "";
		for i = fromPos to lastPos  do (
			if i <= len aStr then
				aResult := aResult ^ [aStr(i)]
			else
				aResult := aResult ^ [fillChar]
		);
		return aResult
	)
pre
	fromPos > 0 and length >= 0;

end String

TestLogger.vdmpp

--$Id: TestLogger.vpp,v 1.2 2006/04/04 07:03:05 vdmtools Exp $
class TestLogger
--テストのログを管理する

values

hisotoryFileName = "VDMTESTLOG.TXT"

functions

public Succeeded: TestCase -> bool
Succeeded(t) == 
	let	Message = t.getTestName()^"\t OK.\n",
		- = new IO().fecho(hisotoryFileName, Message, <append>)	,
		- = new IO().echo(Message)		in
	true;

public Failed: TestCase -> bool
Failed(t) == 
	let	Message = t.getTestName()^"\t NG.\n",
		- = new IO().fecho(hisotoryFileName, Message, <append>),
		- = new IO().echo( Message)		in
	false;

public succeededInAllTestcases : seq of char -> bool
succeededInAllTestcases(m) ==
	let	Message = m ^ "\t OK!!\n",
		- = new IO().fecho(hisotoryFileName, Message, <append>),
		- = new IO().echo( Message)
	in
	true;
	
public notSucceededInAllTestcases :  seq of char -> bool
notSucceededInAllTestcases(m) ==
	let	Message = m ^ "\t NG!!\n",
		- = new IO().fecho(hisotoryFileName,  Message, <append>),
		- = new IO().echo( Message)
	in
	false;

end TestLogger

TestDriver.vdmpp

class TestDriver
--Super class of TestDriver

functions

--Return all TestCases
public tests : () -> seq of TestCase
tests() == is subclass responsibility;

--Confirm test result
public isOK: TestCase -> bool
isOK(t) ==
	if t.TestACase() then
		new TestLogger().Succeeded(t)
	else
		new TestLogger().Failed(t);

operations

--Test a TestCase sequence.
public run: () ==> bool
run() ==
	let	Message = "Test result of a testcase seaquence.",
		TestcaseSeq = tests()	,
		aResult = [isOK(TestcaseSeq(i)) | i in set inds TestcaseSeq]
		--aResult = new Sequence().fmap[TestCase,bool](isOK)(TestcaseSeq)
	in
	if  forall i in set inds aResult & aResult(i) then
		return new TestLogger().succeededInAllTestcases(Message)
	else
		return new TestLogger().notSucceededInAllTestcases(Message)
	
end TestDriver

DoubleListQueueT.vdmpp

class DoubleListQueueT is subclass of TestDriver
functions
public tests : () -> seq of TestCase
tests () == 
	[ new DoubleListQueueT01()
	];
end DoubleListQueueT

class DoubleListQueueT01 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	q0 = DoubleListQueue`empty[int](),
		q1 = DoubleListQueue`enQueue[int](1, q0),
		q2 = DoubleListQueue`enQueue[int](2, q1),
		q3 = DoubleListQueue`enQueue[int](3, q2),
		h1 = DoubleListQueue`top[int](q3),
		q4 = DoubleListQueue`deQueue[int](q3),
		q5 = DoubleListQueue`enQueue[int](4, q4),
		q6 = DoubleListQueue`enQueue[int](5, q5),
		q7 = DoubleListQueue`deQueue[int](q6),
		q8 = DoubleListQueue`deQueue[int](q7),
		q9 = DoubleListQueue`deQueue[int](q8),
		q10 = DoubleListQueue`deQueue[int](q9),
		h2 = DoubleListQueue`top[int](q10),
		q11 = DoubleListQueue`deQueue[int](q10),
		q12 = DoubleListQueue`fromList[char]("Sahara Shin", DoubleListQueue`empty[char]())
	in
	return
		DoubleListQueue`isEmpty[int](q0) and q0 = mk_([], []) and
		DoubleListQueue`toList[int](q1) = [1] and q1 = mk_([], [1]) and
		DoubleListQueue`toList[int](q2) = [1,2] and q2 = mk_([], [2,1]) and
		DoubleListQueue`toList[int](q3) = [1,2,3] and q3 = mk_([], [3,2,1]) and
		h1 = 1 and
		DoubleListQueue`toList[int](q4) = [2,3] and q4 = mk_([2,3], []) and
		DoubleListQueue`toList[int](q5) = [2,3,4] and q5 = mk_([2,3], [4]) and
		DoubleListQueue`toList[int](q6) = [2,3,4,5] and q6 = mk_([2,3], [5, 4]) and
		DoubleListQueue`toList[int](q7) = [3,4,5] and q7 = mk_([3], [5, 4]) and
		DoubleListQueue`toList[int](q8) = [4,5] and q8 = mk_([], [5, 4]) and
		DoubleListQueue`toList[int](q9) = [5] and q9 = mk_([5], []) and
		DoubleListQueue`toList[int](q10) = [] and DoubleListQueue`isEmpty[int](q10) and q10 = mk_([], []) and
		h2 = nil and
		q11 = nil and
		DoubleListQueue`toList[char](q12) = "Sahara Shin" and q12 = mk_([], "nihS arahaS")
		
;
protected setUp: () ==> ()
setUp() == TestName := "DoubleListQueueT01:\t Test Queue";
protected tearDown: () ==> ()
tearDown() == return;
end DoubleListQueueT01

Set.vdmpp

class Set

functions 
-- Same as VDMUtil`set2seq which is implemented by C++
static public asSequence[@T]: set of @T -> seq of @T
asSequence(aSet) ==  
	cases aSet :
		{}		-> [],
		{x} union xs	-> [x] ^ asSequence[@T](xs)
	end
post
	hasSameElems[@T](RESULT, aSet)
measure cardinality;

static cardinality[@T]: set of @T +> nat
cardinality(aSet) == card aSet;

static public hasSameElems[@T] : (seq of @T) * (set of @T) -> bool
hasSameElems(aSeq,aSet) == (elems aSeq = aSet) and (len aSeq = card aSet);

static public Combinations[@T] : nat1 -> set of @T -> set of set of @T
Combinations(n)(aSet) ==
	{ aElem | aElem in set power aSet & card aElem = n};


static public fmap[@T1,@T2]: (@T1 -> @T2) -> set of @T1 -> set of @T2
fmap(f)(aSet) == {f(s) | s in set aSet};

static public Sum[@T]: set of @T ->  @T
Sum(aSet) == SumAux[@T](aSet)(0)
pre
	is_(aSet, set of int) or is_(aSet, set of nat) or is_(aSet, set of nat1) or
 	is_(aSet, set of real) or is_(aSet, set of rat);

static SumAux[@T] : set of @T -> @T -> @T
SumAux(aSet)(aSum) ==
	cases aSet :
	({})	-> aSum,
	{e} union s->
		SumAux[@T](s)(if is_real(aSum) and is_real(e)
		              then aSum + e
		              else undefined)
	end
pre
	pre_Sum[@T](aSet);

end Set

Number.vdmpp

class Number
 
functions 

static public isComputable[@e]: @e -> bool
isComputable(n) ==
	is_(n,int) or is_(n,nat) or is_(n,nat1) or is_(n,real) or is_(n,rat);

static public min[@e] :( @e * @e -> bool) -> @e -> @e -> @e
min(f)(n1)(n2) == if f(n1,n2) then n1 else n2;
	
static public max[@e] : ( @e * @e -> bool) -> @e -> @e -> @e
max(f)(n1)(n2) == if f(n1,n2) then n2 else n1;
			
end Number

CommonDefinition.vdmpp

class CommonDefinition is subclass of Object

/*
values
public StringOrder	= lambda x : seq of char , y : seq of char & String`LT(x,y);
public NumericOrder	= lambda x : NumericalValue, y : NumericalValue & x < y;
public DateOrder	= lambda x : Date, y : Date & x.LT(y);
public AmountOfMoneyOrder	= lambda x : AmountOfMoney, y : AmountOfMoney & x < y;
*/

functions
public StringOrder : seq of char * seq of char -> bool
StringOrder(x, y) == String`LT(x,y);

public NumericOrder : NumericalValue * NumericalValue -> bool
NumericOrder(x, y) == x < y;

public DateOrder : Date * Date -> bool
DateOrder(x, y) ==  x.LT(y);

public AmountOfMoneyOrder : AmountOfMoney * AmountOfMoney -> bool
AmountOfMoneyOrder(x, y) == x < y;
	
types
public Identifier = seq of char
inv - ==  forall s1, s2 : seq of char, id1, id2 : Identifier & id1 <> id2 => s1 <> s2;
public Quantity = int;
public NumericalValue = int;
public Percent = real
inv p == 0 <= p and p <= 100;
public AmountOfMoney = int;
public NonNegativeAmountOfMoney = nat;
public PositiveAmountOfMoney = nat1;
public AmountOfMoney2 = real
	inv am == new Real().isNDigitsAfterTheDecimalPoint(am,2) ;	-- 2 digits after the decimal point

end CommonDefinition

SequenceT.vdmpp

class SequenceT is subclass of TestDriver
functions
public tests : () -> seq of TestCase
tests() == 
	[ 
	new SequenceT25(), 
	new SequenceT23(), new SequenceT24(),
	new SequenceT19(), new SequenceT20(),
	new SequenceT21(), new SequenceT22(),
	new SequenceT01(), new SequenceT02(),
	new SequenceT03(), new SequenceT04(),
	new SequenceT05(), new SequenceT06(),
	new SequenceT07(), new SequenceT08(),
	new SequenceT09(), new SequenceT10(),
	new SequenceT11(), new SequenceT12(),
	new SequenceT13(), new SequenceT14(),
	new SequenceT15(), new SequenceT16(),
	new SequenceT17(), new SequenceT18()
	];
end SequenceT

class SequenceT01 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	sq = new Sequence()	in
       return (sq.Sum[int]([1,2,3,4,5,6,7,8,9]) = 45 and
       sq.Sum[int]([]) = 0) and
       Sequence`Product[int]([2, 3, 4]) = 24 and
       Sequence`Product[int]([]) = 1
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT01:\t Integer sum and product.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT01

class SequenceT02 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	sq = new Sequence()	in
	return sq.Sum[real]([0.1, 0.2, 0.3, 0.4, 0.5, 0.6, 0.7, 0.8, 0.9]) = 4.5 and
	sq.Sum[real]([]) = 0.0 and
	Sequence`Product[real]([2.0, 3.0, 4.0]) = 24.0 and
	Sequence`Product[real]([]) = 1.0 and
	Sequence`Product[real]([2.1, 3.2, 4.3]) = 2.1 * 3.2 * 4.3
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT02:\t Real sum and product.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT02

class SequenceT03 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	sq = new Sequence()	in
	return sq.isAscendingOrder[int]([1,2,4,4,7,8,8,8]) and
	not sq.isAscendingOrder[real]([1.0,2.0,3.0,1.5])
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT03:\t Test isAscendingOrder (integer and real)";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT03

class SequenceT04 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	sq = new Sequence()	in
	return 
		sq.isDescendingOrder[int]([3,2,2,1,1]) and
		Sequence`isDescendingTotalOrder[int] (lambda x : int, y : int & x < y)([3,2,2,1,1]) and
		Sequence`isDescendingTotalOrder[int] (lambda x : int, y : int & x < y)([3,2,2,1,2]) = false
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT04:\t Test isDescendingTotalOrder (integer).";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT04

class SequenceT05 is subclass of TestCase
types
	public TestType = int|seq of char|char;
	public RecordType ::
		val : int
		str : seq of char
		chr : char;
operations 
public  test: () ==> bool
test() == 
	let	sq = new Sequence(),
		decideOrderFuncSeq =
			[(lambda x : int, y : int & x < y),
			lambda x : seq of char, y : seq of char & String`LT(x,y),
			lambda x : char, y : char & Character`LT(x,y)
			],
		decideOrderFunc =
			lambda x : RecordType, y :  RecordType &
				Sequence`isOrdered[SequenceT05`TestType]
					(decideOrderFuncSeq)([x.val,x.str,x.chr])([y.val,y.str,y.chr])
		in
	return 
		Sequence`sort[int](lambda x : int, y : int & x < y)([3,1,5,4]) = [1,3,4,5] and
		Sequence`sort[seq of char]
			(lambda x : seq of char, y : seq of char & String`LT(x,y))
			(["12", "111", "01"]) = ["01","111","12"] and
		Sequence`sort[SequenceT05`RecordType](decideOrderFunc)
			([mk_RecordType(10,"sahara",'c'),mk_RecordType(10,"sahara",'a')]) =
			[mk_RecordType(10,"sahara",'a'),mk_RecordType(10,"sahara",'c')] and
		sq.isOrdered[SequenceT05`TestType](decideOrderFuncSeq)([3,"123",'a'])([3,"123",'A']) = true and
		sq.isOrdered[SequenceT05`TestType](decideOrderFuncSeq)([3,"123",'a'])([3,"123",'0']) = false and
		sq.isOrdered[int|seq of char|char](decideOrderFuncSeq)([])([]) = false and
		sq.isOrdered[int|seq of char|char](decideOrderFuncSeq)([])([3,"123",'0']) = true and
		sq.isOrdered[int|seq of char|char](decideOrderFuncSeq)([3,"123",'0'])([]) = false
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT05:\t test sort and isOrdered.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT05

class SequenceT06 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	let	sq = new Sequence(),
		decideOrderFunc1 = lambda x : int, y : int & x < y,
		decideOrderFunc2 = lambda x : char, y : char & Character`LT(x,y)		in
	return
		sq.Merge[int](decideOrderFunc1)([1,4,6])([2,3,4,5]) = [1,2,3,4,4,5,6] and
		sq.Merge[char](decideOrderFunc2)("146")("2345") = "1234456" and
		sq.Merge[char](decideOrderFunc2)("")("2345") = "2345" and
		sq.Merge[char](decideOrderFunc2)("146")("") = "146"
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT06:\t Merge sequences.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT06

class SequenceT07 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	let	sq = new Sequence()		in
	return
		sq.take[int](2)([2,3,4,5]) = [2,3] and
		sq.drop[char](5)("Shin Sahara") = "Sahara" and
		sq.last[int]([1,2,3]) = 3 and
		sq.filter[int](lambda x:int & x mod 2 = 0)([1,2,3,4,5,6]) = [2,4,6] and
		Sequence`SubSeq[char](4)(3)("1234567890") = "456" and
		Sequence`flatten[int]([[1,2,3], [3,4], [4,5,6]]) = [ 1,2,3,3,4,4,5,6 ]
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT07:\t Handling sequences.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT07

class SequenceT08 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	return
		Sequence`ascendingOrderSort[int]([3,1,6,4,2,6,5]) = [1,2,3,4,5,6,6] and
		Sequence`descendingOrderSort[int]([3,1,6,4,2,6,5]) = [6,6,5,4,3,2,1] 
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT08:\t Test sort.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT08

class SequenceT09 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	return
		Sequence`compact[[int]]([3,1,6,4,nil,2,6,5,nil]) = [3,1,6,4,2,6,5] and
		Sequence`compact[[int]]([nil,nil]) = [] and
		Sequence`compact[[int]]([]) = [] 
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT09:\t Delete nil elements.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT09

class SequenceT10 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	return
		Sequence`freverse[[int]]([3,1,6,4,nil,2,6,5,nil]) = [nil, 5, 6, 2, nil, 4, 6, 1, 3] and
		Sequence`freverse[[int]]([]) = [] 
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT10:\t Get inverse sequence.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT10

class SequenceT11 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	return
		Sequence`Permutations[[int]]([1,2,3]) =
			{ [ 1,2,3 ],
			  [ 1,3,2 ],
			  [ 2,1,3 ],
			  [ 2,3,1 ],
			  [ 3,1,2 ],
			  [ 3,2,1 ] } and
		Sequence`Permutations[[int]]([]) = {[]}
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT11:\t Get permutation.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT11

class SequenceT12 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	return
		Sequence`isMember[int](2)([1,2,3,4,5,6]) and
		Sequence`isMember[int](0)([1,2,3,4,5,6]) = false and
		Sequence`isMember[int](6)([1,2,3,4,5,6]) and
		Sequence`isAnyMember[int]([6])([1,2,3,4,5,6]) and
		Sequence`isAnyMember[int]([0,7])([1,2,3,4,5,6]) = false and
		Sequence`isAnyMember[int]([4,6])([1,2,3,4,5,6]) and
		Sequence`isAnyMember[int]([])([1,2,3,4,5,6]) = false 
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT12:\t Search sequence.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT12
-------------------------------------------------------------
class SequenceT13 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	return
		Sequence`fmap[int, int](lambda x:int & x mod 3)([1,2,3,4,5])  = [1, 2, 0, 1, 2] and
		Sequence`fmap[seq of char, seq of char]
			(Sequence`take[char](2))(["Shin Sahara", "Hiroshi Sakoh"]) = ["Sh", "Hi"]
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT13:\tTest fmap.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT13
-------------------------------------------------------------
class SequenceT14 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	let	index = Sequence`Index,
		indexAll = Sequence`IndexAll2
	in
	return
		index[int](1)([1,2,3,4,5])  = 1 and
		index[int](5)([1,2,3,4,5])  = 5 and
		index[int](9)([1,2,3,4,5])  = 0 and
		index[char]('b')(['a', 'b', 'c'])  = 2 and
		index[char]('z')(['a', 'b', 'c'])  = 0 and
		indexAll[int](9)([1,2,3,4,5]) = {} and
		indexAll[int](9)([]) = {} and
		indexAll[int](1)([1,2,3,4,1]) = {1,5} and
		indexAll[int](1)([1,2,3,4,1,1]) = {1,5,6} 
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT14:\t Test Index.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT14
-------------------------------------------------------------
class SequenceT15 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	let	avg1 = Sequence`GetAverage[int],
		avg2 = Sequence`GetAverage[real]
	in
	return
		avg1([]) = nil and
		avg1([1,2,3,4]) = (1+2+3+4) / 4 and
		avg2([1.3, 2.4, 3.5]) = 7.2 / 3
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT15:\t Test GetAverage.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT15
-------------------------------------------------------------
class SequenceT16 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	let	ins1 = Sequence`InsertAt[int],
		ins2 = Sequence`InsertAt[char]
	in
	return
		ins1(1)(1)([2,3,4,5]) = [1,2,3,4,5] and
		ins1(3)(3)([1,2,4,5]) = [1,2,3,4,5] and
		ins1(3)(3)([1,2]) = [1,2,3] and
		ins1(4)(3)([1,2]) = [1,2,3] and
		ins1(5)(3)([1,2]) = [1,2,3] and
		ins2(1)('1')("2345") = "12345" and
		ins2(3)('3')("1245") = "12345" and
		ins2(3)('3')("12") = "123"
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT16:\t Test InsertAt.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT16
-------------------------------------------------------------
class SequenceT17 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	let	rm1 = Sequence`RemoveAt[int],
		rm2 = Sequence`RemoveAt[char]
	in
	return
		rm1(1)([1,2,3,4,5]) = [2,3,4,5] and
		rm1(3)([1,2,4,3]) = [1,2,3] and
		rm1(3)([1,2]) = [1,2] and
		rm1(4)([1,2]) = [1,2] and
		rm1(5)([1,2]) = [1,2] and
		rm2(1)("12345") = "2345" and
		rm2(3)("1243") = "123" and
		rm2(3)("12") = "12"
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT17:\t Test RemoveAt.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT17
-------------------------------------------------------------
class SequenceT18 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	let	up1 = Sequence`UpdateAt[int],
		up2 = Sequence`UpdateAt[char]
	in
	return
		up1(1)(10)([1,2,3,4,5]) = [10,2,3,4,5] and
		up1(3)(40)([1,2,4,3]) = [1,2,40,3] and
		up1(2)(30)([1,2]) = [1,30] and
		up1(3)(30)([1,2]) = [1,2] and
		up1(4)(30)([1,2]) = [1,2] and
		up2(1)('a')("12345") = "a2345" and
		up2(3)('b')("1243") = "12b3" and
		up2(3)('c')("123") = "12c" and
		up2(3)('c')("12") = "12"
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT18:\t Test UpdateAt.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT18
-------------------------------------------------------------
class SequenceT19 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	let	removeDup = Sequence`RemoveDup[int],
		removeMember = Sequence`RemoveMember[int],
		removeMembers = Sequence`RemoveMembers[int]
	in
	return
		removeDup([]) = [] and
		removeDup([1,1,2,2,2,3,4,4,4,4]) = [1,2,3,4] and
		removeDup([1,2,3,4]) = [1,2,3,4] and
		removeMember(1)([]) = [] and
		removeMember(1)([1,2,3]) = [2,3] and
		removeMember(4)([1,2,3]) = [1,2,3] and
		removeMembers([])([]) = [] and
		removeMembers([])([1,2,3]) = [1,2,3] and
		removeMembers([1,2,3])([]) = [] and
		removeMembers([1,2,3])([1,2,3]) = [] and
		removeMembers([1,4,5])([1,2,3,4]) = [2,3] 
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT19:\t Test removes.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT19
-------------------------------------------------------------
class SequenceT20 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	let	zip = Sequence`Zip[int, char],
		zip2 = Sequence`Zip2[int,char],
		unzip = Sequence`Unzip[int, char]
	in
	return
		zip([], []) = [] and
		zip([1,2,3], ['a', 'b', 'c']) = [mk_(1, 'a'), mk_(2, 'b'), mk_(3, 'c')] and
		zip([1,2], ['a', 'b', 'c']) = [mk_(1, 'a'), mk_(2, 'b')] and
		zip([1,2,3], ['a', 'b']) = [mk_(1, 'a'), mk_(2, 'b')] and
		zip2([])([]) = [] and
		zip2([1,2,3])(['a', 'b', 'c']) = [mk_(1, 'a'), mk_(2, 'b'), mk_(3, 'c')] and
		unzip([]) = mk_([], []) and
		unzip([mk_(1, 'a'), mk_(2, 'b'), mk_(3, 'c')]) = mk_([1,2,3], ['a', 'b', 'c']) 
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT20:\t Test zip related functions.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT20
-------------------------------------------------------------
class SequenceT21 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	let	span = Sequence`Span[int],
		p1 = lambda x : int & x mod 2 = 0,
		p2 = lambda x : int & x < 10
 	in
	return
		span(p1)([]) = mk_([], []) and
		span(p1)([2,4,6,1,3]) = mk_([2,4,6], [1,3]) and
		span(p2)([1,2,3,4,5]) = mk_([1,2,3,4,5], []) and
		span(p2)([1,2,12,13,4,15]) = mk_([1,2], [12,13,4,15])
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT21:\t Test span.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT21
-------------------------------------------------------------
class SequenceT22 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	let	takeWhile = Sequence`TakeWhile[int],
		dropWhile = Sequence`DropWhile[int],
		p1 = lambda x : int & x mod 2 = 0
 	in
	return
		takeWhile(p1)([]) = [] and
		takeWhile(p1)([2,4,6,8,1,3,5,2,4]) = [2,4,6,8] and
		dropWhile(p1)([]) = [] and
		dropWhile(p1)([2,4,6,8,1,2,3,4,5]) = [1,2,3,4,5] 
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT22:\t Test TakeWhile and DropWhile.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT22
-------------------------------------------------------------
class SequenceT23 is subclass of TestCase
functions
public plus : int -> int -> int
plus(a)(b) == a + b;

public product : int -> int -> int
product(a)(b) == a * b;

public append : seq of char -> char -> seq of char
append(s)(e) == s ^ [e];

operations 
public  test: () ==> bool
test() == 
	let	foldl = Sequence`Foldl[int, int],
		f2 = Sequence`Foldl[seq of char, char]
 	in
	return
		foldl(plus)(0)([1,2,3]) = 6 and
		foldl(product)(1)([2,3,4]) = 24 and
		f2(append)([])("abc") = "abc" 
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT23:\t Test Foldl.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT23
-------------------------------------------------------------
class SequenceT24 is subclass of TestCase
functions
public plus : int -> int -> int
plus(a)(b) == a + b;

public product : int -> int -> int
product(a)(b) == a * b;
operations 
public  test: () ==> bool
test() == 
	let	removeAt = Sequence`RemoveAt[char],
		foldr = Sequence`Foldr[int, int],
		f3 = Sequence`Foldr[nat1, seq of char]
 	in
	return
		foldr(plus)(0)([1,2,3]) = 6 and
		foldr(product)(1)([2,3,4]) = 24 and
		f3(removeAt)("12345")([1,3,5]) = "24"
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT24:\t Test Foldr.";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT24
-------------------------------------------------------------
class SequenceT25 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	let	sq = new Sequence()	in
	return
		Real`EQ(sq.GetAverage[real]([1.1,2.2,3.3]))(2.2) and
		Real`EQ(sq.GetAverage[real]([1,2,3,4,5,6,7,8,9,10]))(5.5)
;
protected setUp: () ==> ()
setUp() == TestName := "SequenceT25:\t Test GetAverage";
protected tearDown: () ==> ()
tearDown() == return;
end SequenceT25

Character.vdmpp

class Character

values
--vNumEnglishChars = "0123456789aAbBcCdDeEfFgGhHiIjJkKlLmMnNoOpPqQrRsStTuUvVwWxXyYzZ";
vNumOrderMap = 
	{'0' |-> 1, '1' |-> 2, '2' |-> 3, '3' |-> 4, '4' |-> 5, '5' |-> 6, '6' |-> 7, '7' |-> 8, '8' |-> 9, '9' |-> 10};

vChapitalCharOrderMap =
	{'A' |-> 12, 'B' |-> 14, 'C' |-> 16, 'D' |-> 18, 'E' |-> 20, 'F' |-> 22, 'G' |-> 24, 'H' |-> 26, 'I' |-> 28, 
	'J' |-> 30, 'K' |-> 32, 'L' |-> 34, 'M' |-> 36, 'N' |-> 38, 'O' |-> 40, 'P' |-> 42, 'Q' |-> 44, 'R' |-> 46,
	'S' |-> 48, 'T' |-> 50, 'U' |-> 52, 'V' |-> 54, 'W' |-> 56, 'X' |-> 58, 'Y' |-> 60, 'Z' |-> 62};

vSmallCharOrderMap =
	{'a' |-> 11, 'b' |-> 13, 'c' |-> 15, 'd' |-> 17, 'e' |-> 19, 'f' |-> 21, 'g' |-> 23, 'h' |-> 25, 'i' |-> 27,
	'j' |-> 29, 'k' |-> 31, 'l' |-> 33, 'm' |-> 35, 'n' |-> 37, 'o' |-> 39, 'p' |-> 41, 'q' |-> 43, 'r' |-> 45, 
	's' |-> 47, 't' |-> 49, 'u' |-> 51, 'v' |-> 53, 'w' |-> 55, 'x' |-> 57, 'y' |-> 59, 'z' |-> 61};

vCharOrderMap = vNumOrderMap munion vChapitalCharOrderMap munion vSmallCharOrderMap;

functions
/* Converted from vNumEnglishChars to vCharOrderMap
static public makeOrderMap : seq of char +> map char to nat
makeOrderMap(s) ==
	{s(i) |-> i | i in set inds s};
*/

static public asDigit: char -> int | bool
asDigit(c) ==
	if isDigit(c) then
		let s = [c] in
		let mk_(-, i) = VDMUtil`seq_of_char2val[int](s) in i
	else
		false;

static public asDictOrder : char -> int
asDictOrder(c) == 
	if c in set dom vCharOrderMap then
		vCharOrderMap(c)
	else
		let nonAsciiChar = 999999 in nonAsciiChar;

static public isDigit : char -> bool
isDigit(c) == c in set dom vNumOrderMap;

static public isLetter : char -> bool
isLetter(c) == c in set dom (vChapitalCharOrderMap munion vSmallCharOrderMap);

static public isLetterOrDigit : char -> bool
isLetterOrDigit(c) == isDigit(c) or isLetter(c);

static public isCapitalLetter : char -> bool
isCapitalLetter(c) == c in set dom vChapitalCharOrderMap;

static public isLowercaseLetter : char -> bool
isLowercaseLetter(c) == c in set dom vSmallCharOrderMap;

static public LT: char * char -> bool
LT(c1,c2) == Character`LT2(c1)(c2);

static public LT2: char -> char -> bool
LT2(c1)(c2) == Character`asDictOrder(c1) < Character`asDictOrder(c2);

static public LE : char * char -> bool
LE(c1, c2) == Character`LE2(c1)(c2);

static public LE2 : char -> char -> bool
LE2(c1)(c2) ==  Character`LT2(c1)(c2) or c1 = c2;

static public GT : char * char -> bool
GT(c1, c2) == Character`GT2(c1)(c2);

static public GT2 : char -> char -> bool
GT2(c1)(c2) == Character`LT2(c2)(c1);

static public GE : char * char -> bool
GE(c1, c2) == Character`GE2(c1)(c2);

static public GE2 : char -> char -> bool
GE2(c1)(c2) == not Character`LT2(c1)(c2);
			
end Character

DoubleListQueue.vdmpp

/*   
 * Queue using 2 sequences.
 * Usage:
 *	make empty queue as following:
 * 		let Q0 = DoubleListQueue`empty[int]() in ...
 *	
 *	append an element to queue:
 *		DoubleListQueue`enQueue(1, Q0)
 *	
*/

class DoubleListQueue

functions
static public empty[@T] : () -> seq of @T * seq of @T
empty() == mk_([], []);

static public isEmpty[@T] : (seq of @T * seq of @T) -> bool
isEmpty(s) == s = mk_([], []);

static public enQueue[@T] : @T * (seq of @T * seq of @T) -> seq of @T * seq of @T
enQueue(anElem, mk_(aHeads, aTails)) == mk_(aHeads, [anElem] ^ aTails);

static public deQueue[@T] : (seq of @T * seq of @T) -> [seq of @T * seq of @T]
deQueue(mk_(aHeads, aTails)) == 
	cases aHeads:
		[-] ^ aTailsOfHeads	-> mk_(aTailsOfHeads, aTails),
		[]	-> 
			cases aTails:
				[]		-> nil,
				others	-> mk_(tl Sequence`freverse[@T](aTails), [])
			end
	end;

static public top[@T] : (seq of @T * seq of @T) -> [@T]
top(mk_(aHeads, aTails)) == 
	cases aHeads:
		[h] ^ -	-> h,
		[]	-> 
			cases aTails:
				[]		-> nil,
				others	-> hd Sequence`freverse[@T](aTails)
			end
	end;

static public fromList[@T] : seq of @T * (seq of @T * seq of @T) -> seq of @T * seq of @T
fromList(aSeq, aQueue) ==
	cases aSeq:
		[]				-> aQueue,
		[h] ^ aTailsOfSeq		-> fromList[@T](aTailsOfSeq, enQueue[@T](h, aQueue))
	end
measure fromListMeasure;

static fromListMeasure[@T] : seq of @T *  (seq of @T * seq of @T) +> nat
fromListMeasure(s, -) == len s;

static public toList[@T] : (seq of @T * seq of @T) -> seq of @T
toList(aaQueue) ==
	cases aaQueue:
		(mk_([], []))	-> [],
		aQueue	-> [top[@T](aQueue)] ^ toList[@T](deQueue[@T](aQueue))
	end
measure toListMeasure;

static toListMeasure[@T] :  (seq of @T * seq of @T) +> nat
toListMeasure(mk_(s1, s2)) == len s1 + len s2;

end DoubleListQueue

SetT.vdmpp

class SetT is subclass of TestDriver
functions
public tests : () -> seq of TestCase
tests () == 
	[
		new SetT01(),
		new SetT02(),
		new SetT03(),
		new SetT04()
	];
end SetT
----------------------------------------
class SetT01 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	return
		Set`hasSameElems[int](Set`asSequence[int]({1,2,3,4}),{1,2,3,4}) and
		(elems Set`asSequence[int]({1,2,3,3,4}) = {1,2,3,4})
;
protected setUp: () ==> ()
setUp() == TestName := "SetT01:\t Compare sequences and convert to sequence.";
protected tearDown: () ==> ()
tearDown() == return;
end SetT01
----------------------------------------

class SetT02 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	return
		Set`Combinations[int](2)({1,2,3}) = { { 1,2 }, { 1,3 }, { 2,3 } } and
		Set`Combinations[int](2)({1,2,3,4}) = { { 1,2 },  { 1,3 },  { 1,4 },  { 2,3 },  { 2,4 },  { 3,4 } } and
		Set`fmap[set of int, set of set of int](Set`Combinations[int](2))({{1,2,3}, {1,2,3,4}}) =
			{{ { 1,2 }, { 1,3 }, { 2,3 } }, { { 1,2 },  { 1,3 },  { 1,4 },  { 2,3 },  { 2,4 },  { 3,4 } } } and
		Set`Combinations[int](3)({1,2,3,4}) = { { 1,2,3 },  { 1,2,4 },  { 1,3,4 },  { 2,3,4 } } and
		Set`Combinations[seq of char](2)({"Sahara", "Sato", "Sakoh", "Yatsu", "Nishikawa" }) = 
			{ { "Sahara",    "Sato" },  { "Sahara",    "Nishikawa" },  { "Sahara",    "Yatsu" },  { "Sahara",    "Sakoh" },  { "Sato",    "Nishikawa" }, 
			{ "Sato",    "Yatsu" },  { "Sato",    "Sakoh" },  { "Nishikawa",    "Yatsu" },  { "Nishikawa",    "Sakoh" },  { "Yatsu",    "Sakoh" } }
;
protected setUp: () ==> ()
setUp() == TestName := "SetT02:\t Get combination.";
protected tearDown: () ==> ()
tearDown() == return;
end SetT02
-------------------------------------------------------------

class SetT03 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	return
		Set`fmap[int, int](lambda x:int & x mod 3)({1,2,3,4,5})  = {0, 1, 2} and
		Set`fmap[seq of char, seq of char]
			(Sequence`take[char](2))({"Shin Sahara", "Hiroshi Sakoh"}) = {"Sh", "Hi"}
;
protected setUp: () ==> ()
setUp() == TestName := "SetT03:\t Test fmap.";
protected tearDown: () ==> ()
tearDown() == return;
end SetT03
-------------------------------------------------------------

class SetT04 is subclass of TestCase
operations 
public  test: () ==> bool
test() == 
	return
		Set`Sum[int]({1,...,10}) = 55 and
		Set`Sum[int]({1, 2, 3, 4, 5, 6, 7, 8,  9, 10}) = 55 and
		abs(Set`Sum[real]({0.1, 0.2, 0.3}) - 0.6) <= 1E-5 and
		Set`Sum[nat]({1, 2, 3, 3}) = 6
;
protected setUp: () ==> ()
setUp() == TestName := "SetT04:\tTest sum of set elements.";
protected tearDown: () ==> ()
tearDown() == return;
end SetT04

Hashtable.vdmpp

/* Responsibility:
 *	Hash Table
 
 * Usage:
 *	(1) Object in Hashtable have to have hashCode() function and equals() function.
 
 * From historical reason, there are functional programming style and object-oriented style functions.
 * if function name starts chapital letter, the function is functional programming style
 * else the function is object-oriented style.
*/
class Hashtable is subclass of CommonDefinition 

types
public Contents = map Object to Object;
public Bucket = map int to Contents;

instance variables
sBucket : Bucket := { |->};

operations

public Hashtable : () ==> Hashtable
Hashtable() == 
	(
	sBucket := { |-> };
	return self
	);
	
public Hashtable : Contents ==> Hashtable
Hashtable(aContents) == 
	(
	self.putAll(aContents);
	return self
	);

--Hashtableのクリアー
public clear : () ==> ()
clear() == setBuckets({ |-> });

public getBuckets : () ==> Bucket 
getBuckets() == return sBucket;

public setBuckets : Bucket ==> ()
setBuckets(aBucket) == sBucket := aBucket;

public keySet : () ==> set of Object
keySet() ==
	let	buckets = self.getBuckets()
	in
	(
	dcl allKeySet : set of Object := {};
	for all aContents in set rng buckets do
		allKeySet := allKeySet union dom aContents;
	return allKeySet
	);

public put : Object * Object ==> ()
put(akey, aValue) ==
	let	buckets = self.getBuckets(),
		hashcode = akey.hashCode()
	in
	(
	if hashcode in set dom buckets then
		self.setBuckets(buckets ++ {hashcode |-> (buckets(hashcode) ++ {akey |-> aValue})})
	else
		self.setBuckets(buckets munion {hashcode |-> {akey |-> aValue}})
	);

public putAll : Contents ==> ()
putAll(aContents) == 
	for all key in set dom aContents do (
		self.put(key, aContents(key))
	);

public get : Object  ==> [Object]
get(key) ==
	let	buckets = self.getBuckets(),
		hashcode = key.hashCode()
	in
	(
	if hashcode in set dom buckets then
		let	aContents = buckets(hashcode)
		in
		for all aKey in set dom aContents do (
			if key.equals(aKey) then
				return aContents(aKey)
		);
	return nil
	);

public remove : Object ==> [Object]
remove(key) ==
	let	buckets = self.getBuckets(),
		hashcode = key.hashCode(),
		deleteObj = self.get(key)
	in
	(
	if deleteObj <> nil then
		let	aContents = buckets(hashcode),
			newContents = aContents :-> {deleteObj}
		in
		(
		self.setBuckets(buckets ++ {hashcode |-> newContents});
		return deleteObj
		)
	else
		return nil
	);

public valueSet : () ==> set of Object
valueSet() ==
	let	buckets = self.getBuckets()
	in
	(
	dcl aValueSet : set of Object := {};
	for all aContents in set rng buckets do
		aValueSet := aValueSet union rng aContents;
	return aValueSet
	);

functions

public size : () -> nat
size() == card self.keySet();

public isEmpty : () -> bool
isEmpty() == self.keySet() = {};
		
public contains : Object -> bool
contains(anObject) ==
	let	buckets = self.getBuckets()
	in
	exists hashcode in set dom buckets &
		let	aContents = buckets(hashcode)
		in
		exists key in set dom aContents &
			 aContents(key).equals(anObject);
		
public containsKey : Object -> bool
containsKey(aKey) ==
	let	buckets = self.getBuckets()
	in
	exists hashcode in set dom buckets & 
		exists key in set dom buckets(hashcode) &
			aKey.equals(key);


-----------Functional Programming part

functions

static public Put[@T1, @T2] : 
	(map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> @T1 -> @T2 
	-> (map @T1 to (map @T1 to  @T2))
Put(aHashtable)(aHashCode)(aKey)(aValue) ==
	let	hashcode = aHashCode(aKey)
	in
	if hashcode in set dom aHashtable then
		aHashtable ++ {hashcode |-> (aHashtable(hashcode) ++ {aKey |-> aValue})}
	else
		aHashtable munion {hashcode |-> {aKey |-> aValue}}
	;

static public PutAll[@T1, @T2] : 
	(map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> (map @T1 to  @T2) 
	-> (map @T1 to (map @T1 to  @T2)) 
PutAll(aHashtable)(aHashCode)(aMap) == 
	PutAllAux[@T1, @T2](aHashtable)(aHashCode)(aMap)(dom aMap);

static public PutAllAux[@T1, @T2] :
	(map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> (map @T1 to  @T2)  -> set of @T1
	-> (map @T1 to (map @T1 to  @T2)) 
PutAllAux(aHashtable)(aHashCode)(aMap)(aKeySet) ==
	if aKeySet = {} then
		aHashtable
	else
		let	aKey in set aKeySet	in
		let	newHashtable = Put[@T1, @T2](aHashtable)(aHashCode)(aKey)(aMap(aKey))	
		in
		PutAllAux[@T1, @T2](newHashtable)(aHashCode)(aMap)(aKeySet \ {aKey})
	;

static public Get[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> @T1  -> [@T2]
Get(aHashtable)(aHashCode)(aKey) ==
	let	hashcode = aHashCode(aKey)
	in
	if hashcode in set dom aHashtable then
		Map`Get[@T1, @T2](aHashtable(hashcode))(aKey)
	else
		nil
	;

static public Remove[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> @T1 -> (map @T1 to (map @T1 to  @T2))
Remove(aHashtable)(aHashCode)(aKey) == 
	let	hashcode = aHashCode(aKey)
	in
	{h |-> ({aKey} <-: aHashtable(hashcode)) | h in set {hashcode}} munion 
		{hashcode} <-: aHashtable ;

--Hashtableのクリアー
static public Clear[@T1, @T2] : () -> (map @T1 to (map @T1 to  @T2))
Clear() == ({ |-> });

static public KeySet[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> set of  @T1
KeySet(aHashtable) == 
	--let	aMapSet = rng aHashtable,
		--f = lambda x : map @T1 to  @T2 & dom x
	let	aMapSet = rng aHashtable
	in
	if aMapSet <> {} then
		--dunion Set`fmap[map @T1 to  @T2, @T2](f)(aMapSet)
		dunion  {dom s | s in set aMapSet} 
	else
		{};

static public ValueSet[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> set of  @T2
ValueSet(aHashtable) == 
	--let	aMapSet = rng aHashtable,
		--f = lambda x : map @T1 to  @T2 & rng x
	let	aMapSet = rng aHashtable
	in
	if aMapSet <> {} then
		--dunion Set`fmap[map @T1 to  @T2, @T2](f)(aMapSet)
		dunion  {rng s | s in set aMapSet} 
	else
		{};
	
static public Size[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> nat
Size(aHashtable) == card KeySet[@T1, @T2](aHashtable) ;

static public IsEmpty[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> bool
IsEmpty(aHashtable) == KeySet[@T1, @T2](aHashtable) = {};
		
static public Contains[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> @T2 -> bool
Contains(aHashtable)(aValue) == 
	let	aMapSet = rng aHashtable	
	in
	if aMapSet <> {} then
		exists aMap in set aMapSet & aValue in set rng aMap
	else
		false;
		
static public ContainsKey[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> @T1 -> bool
ContainsKey(aHashtable)(aKey) == 
	let	aMapSet = rng aHashtable	
	in
	if aMapSet <> {} then
		exists aMap in set aMapSet & aKey in set dom aMap
	else
		false;

end Hashtable

DateT.vdmpp

class DateT is subclass of TestDriver 
functions
public tests : () -> seq of TestCase
tests() == 
	[ new DateT01(), new DateT02(), new DateT03(), 
	new DateT04(),
	new DateT05(), new DateT06(),new DateT07()
	];
end DateT

class DateT01 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar(),
		d = jc.getDateFrom_yyyy_mm_dd(2001,5,1)	,
		d1 = jc.getDateFrom_yyyy_mm_dd(2001,4,29),
		d2 = jc.getDateFrom_yyyy_mm_dd(2001,4,28)
	in
	return
		d.getNumberOfDayOfTheWeek() = jc.getNumberOfDayOfTheWeekFromName(<Tue>) and
		d.getNameOfDayOfTheWeek() = <Tue> and
		d1.getNameOfDayOfTheWeek() = <Sun> and
		d2.getNameOfDayOfTheWeek() = <Sat> and
		d.isSunday() = false and
		d.isSaturday() = false and
		d.isWeekday() = true and
		d.isDayOff() = false and 
		d.isNotDayOff() = true and
		d.isSundayOrDayoff()  = false
	;
protected setUp: () ==> ()
setUp() == TestName := "DateT01:\tCalculate the day of the week.";
protected tearDown: () ==> ()
tearDown() == return;
end DateT01

class DateT02 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar(),
		d = jc.getDateFrom_yyyy_mm_dd(2001,5,1)		in
	return
		d.get_yyyy_mm_dd() = mk_(2001,5,1) and
		d.date2Str() = "20010501" and
		d.asString() = "20010501" and
		d.print() = "Year=2001, Month=05, Day=01, "
	;
protected setUp: () ==> ()
setUp() == TestName := "DateT02:\tConvert date.";
protected tearDown: () ==> ()
tearDown() == return;
end DateT02

class DateT03 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar(),
		d20000101 = jc.getDateFromString("20000101"),
		d0301 = jc.getDateFromString("20010301"),
		d0501 = jc.getDateFromString("20010501"),
		d0711 = jc.getDateFrom_yyyy_mm_dd(2001,7,11)	in
	return
		d0301.getTheNumberOfDayOff(d0711)  = 24 and
		d0501.getTheNumberOfDayOffExceptStartDate(d0711) = 13 and
		d20000101.getTheNumberOfDayOff(d0711)  = 103
	;
protected setUp: () ==> ()
setUp() == TestName := "DateT03:\tgetTheNumberOfDayOff";
protected tearDown: () ==> ()
tearDown() == return;
end DateT03

class DateT04 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar(),
		d20001231 = jc.getDateFrom_yyyy_mm_dd(2000,12,31),
		d1231 = jc.getDateFrom_yyyy_mm_dd(2001,12,31),
		d0626 = jc.getDateFrom_yyyy_mm_dd(2001,6,26),
		d0501 = jc.getDateFromString("20010501"),
		d0505 = jc.getDateFromString("20010505"),
		d0502 = jc.getDateFrom_yyyy_mm_dd(2001,5,2)		in
	return
		d0502.addWeekday(1).getFutureWeekday().date2Str() = "20010507" and
		d0502.getPastWeekday().subtractWeekday(1).date2Str() = "20010501" and
		d0501.getPastWeekday().subtractWeekday(1).date2Str() = "20010427" and
		d0501.getFutureWeekday().date2Str() = "20010501" and
		d0501.addWeekday(2).date2Str() = "20010507" and
		d0502.subtractWeekday(2).date2Str() = "20010427" and
		d1231.daysFromNewYear() = 365 and
		d20001231.daysFromNewYear() = 366 and
		d0501.getNumberOfTheDayOfWeek(d0626,<Tue>) = 9 and
		jc.getFutureWeekday(d0505).date2Str() = "20010507" and
		jc.getFutureWeekday(d0501).date2Str() = "20010501" and
		jc.getPastWeekday(d0501).date2Str() = "20010501" and
		jc.getPastWeekday(d0505).date2Str() = "20010502" 
	;
protected setUp: () ==> ()
setUp() == TestName := "DateT04:\tCalculate date.";
protected tearDown: () ==> ()
tearDown() == return;
end DateT04

class DateT05 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar(),
		d0711 = jc.getDateFromString("20010711")	in
	(
	jc.setToday(jc.getDateFrom_yyyy_mm_dd(2001, 3, 1));
	let	d0301 = jc.today()	in
	return
		d0711.EQ(jc.getDateFrom_yyyy_mm_dd(2001, 7, 11)) and
		d0711.NE(jc.getDateFrom_yyyy_mm_dd(2001, 7, 12)) and
		jc.EQ(d0711,jc.getDateFrom_yyyy_mm_dd(2001, 7, 11)) and
		d0301.LT(d0711) and
		jc.LT(d0301, d0711) and
		d0711.GT(d0301) and
		jc.GT(d0711,d0301) and
		d0711.GE(d0711) and d0711.GE(d0301) and
		jc.GE(d0711,d0711)  and jc.GE(d0711,d0301) and
		d0711.LE(d0711) and d0301.LE(d0711) and
		jc.LE(d0711,d0711) and jc.LE(d0301,d0711)
	);
protected setUp: () ==> ()
setUp() == TestName := "DateT05:\tCompare date.date";
protected tearDown: () ==> ()
tearDown() == return;
end DateT05

class DateT06 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar(),
		d10010301 = jc.getDateFromString("10010301"),
		d0711 = jc.getDateFromString("20010711")	in
	(
	jc.setToday(jc.getDateFrom_yyyy_mm_dd(2001, 3, 1));
	let	d0301 = jc.today()		in
	return
		jc.firstDayOfTheWeekInMonth(2000,3,<Wed>).get_yyyy_mm_dd() = mk_( 2000,3,1 ) and
		jc.firstDayOfTheWeekInMonth(2001,7,<Sun>).get_yyyy_mm_dd() = mk_( 2001,7,1 ) and
		jc.lastDayOfTheWeekInMonth(2000,2,<Tue>).get_yyyy_mm_dd() = mk_( 2000,2,29 ) and
		jc.lastDayOfTheWeekInMonth(2001,7,<Sun>).get_yyyy_mm_dd() = mk_( 2001,7,29 ) and
		jc.getNthDayOfTheWeek(2001,7,5,<Sun>).get_yyyy_mm_dd() = mk_( 2001,7,29 ) and
		jc.getNthDayOfTheWeek(2001,7,6,<Sun>) = false and
		jc.getNumberOfTheDayOfWeek(d0711,d0301,<Sun>)  = 19 and
		jc.getNumberOfTheDayOfWeek(d0711,d10010301,<Sun>)  = 52196	
	);
protected setUp: () ==> ()
setUp() == TestName := "DateT06:\tGet the day of the week.";
protected tearDown: () ==> ()
tearDown() == return;
end DateT06

class DateT07 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
	let	jc = new JapaneseCalendar()	in
	return
		jc.isLeapYear(2000) = true and
		jc.isLeapYear(2001) = false and
		jc.isLeapYear(1996) = true and
		jc.isLeapYear(1900) = false and
		jc.isLeapYear(1600) = true and
		jc.isDateString("sahara") = false and
		jc.isDateString("20010723") = true and
		jc.isDateString("20011232") = false and
		jc.isWeekday(<Mon>) = true and
		jc.isWeekday(<Tue>) = true and
		jc.isWeekday(<Wed>) = true and
		jc.isWeekday(<Thu>) = true and
		jc.isWeekday(<Fri>) = true and
		jc.isWeekday(<Sat>) = false and
		jc.isWeekday(<Sun>) = false and
		jc.date2Str(jc.getLastDayOfMonth(2000,2)) = "20000229" and
		jc.date2Str(jc.getLastDayOfMonth(2001,2)) = "20010228"
	;
protected setUp: () ==> ()
setUp() == TestName := "DateT07:\tQuery about date.date";
protected tearDown: () ==> ()
tearDown() == return;
end DateT07