Quellcode-Bibliothek FO.vdmpp

class FO is subclass of GLOBAL

instance variables 
  id    : FOId;
  coord : Coordinates;
  alt   : Altitude;  
  
 
operations

public FO : FOId * Coordinates * Altitude ==> FO
FO(i,c,a) == 
 (id := i;
  coord := c;
  alt := a;
 );
    
pure public getId : () ==> FOId
getId() ==
  return id;

public getCoordinates : () ==> Coordinates
getCoordinates() == 
  return coord;

public setCoordinates : Coordinates ==> ()
setCoordinates(c) ==
  coord := c;
  
public getAltitude : () ==> Altitude
getAltitude() ==
  return alt;
    
public setAltitude : Altitude ==> ()
setAltitude(a) ==
  alt := a;
 
public getPosition : () ==> Position
getPosition() == 
  return mk_Position(coord,alt); 
  

end FO