lifepoint.dcl

DEFINITION MODULE lifepoint;
IMPORT lifemisc;

TYPE
:: Pnt -> (!INT,!INT);
:: PntList -> [!Pnt];
:: Rect -> (!Pnt, !Pnt); 
:: Lifestats -> (!INT, !INT, !INT, !INT, !INT, !INT);

RULE
:: Same !PntList !PntList -> BOOL;
:: SwapPnt !INT !INT !PntList -> PntList;
:: SortPnt !PntList -> PntList;
:: CropPnt !INT !INT !INT !INT !PntList -> PntList;
:: StatPnt !PntList -> (!INT, !Lifestats);
:: Step !PntList -> PntList;

Back to tutorial