GetSensors : THEORY

  BEGIN

  AI: ARRAY[subrange(1,64)->real]

  Sensor_t: TYPE = {Power, Pressure, Temperature}

  GetSensor(Sensor:Sensor_t,N:int):ARRAY[subrange(1,N)->real]=
      COND 
	Sensor=Power -> LAMBDA(i:subrange(1,4)):AI(i+5),
	Sensor=Pressure -> LAMBDA(i:subrange(1,2)):AI(i+61),
	Sensor=Temperature -> LAMBDA(i:subrange(1,3)):AI(i)
      ENDCOND

  END GetSensors


sum: THEORY
 BEGIN

 n: VAR nat

 sum(n): RECURSIVE nat =
  (IF n = 0 THEN 0 ELSE n + sum(n - 1) ENDIF)
  MEASURE id

 closed_form: THEOREM sum(n) = (n * (n + 1))/2

 END sum