marks.mch

这里几个源代码是用BToolkit软件写的。这是关于一些操作

MACHINE           Marks(mmax)	
	  
CONSTRAINTS 	  mmax:NAT1

VARIABLES         record

INVARIANT         record : 0..mmax --> NAT
		  

INITIALISATION    record := {}

OPERATIONS

  addmark(mm:NAT) =
		PRE mm :0..mmax
		THEN
		IF mm:dom(record)
		THEN record(mm) := record(mm)+1
		ELSE record:=record \/{mm |->1}
		END
		END

END