FormalMethod/student.vpp at master · azmanuddin94/FormalMethod · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
class student

types
	public month = <january>|<february>|<march>|<april>|<may>|<june>|<july>|<august>|<september>|<october>|<november>|<december>;
	public Day = nat1
	inv d == d < 31;
	public date = Day * month * year ;
	public course = seq of char * seq of char * nat;

	public number = nat;
	public streetName = seq of char;
	public state = <Sarawak>|<Sabah>|<WPKL>|<WPLB>|<Pahang>|<Perak>|<Melaka>|<Terengganu>|<Johor>|<Kelantan>|<NSembilan>|<Perlis>|<Kedah>|<>;

	public address = nat * seq of char * nat * seq of char;
	public address = number * streetName * postcode * state;
	public constHour =

Composite/Record Type
	[access] indentifier :: identifier : Type

	public address :: number : nat
					  streetName : seq of char
					  postcode : nat
					  state : State; //refer to type state
					  year : nat; //no definition for year, use nat
Operation
	[access] operationName : Type * Type ==> Type
	operationName (a,b) ==
	(
		statements
	)
	[pre]
	[post]
end student

public setYearOfStudy : Year ==> Year
setYearOfStudy (CurrentYear) ==
(
	yearOfStudy := CurrentYear;
	return yearOfstudy;
);

public boolean isNumber(int abc){

}