Advertisement
DanielDv99

TEMPERATURE

Sep 25th, 2017
1,080
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. note
  2.     description: "Temperature."
  3.  
  4. class
  5.     TEMPERATURE
  6.  
  7. create
  8.     make_celsius, make_kelvin
  9.  
  10. feature -- Initialization
  11.  
  12.     make_celsius (v: INTEGER)
  13.             -- Create with Celsius value `v'.
  14.         require
  15.                 temperature_is_valid : v >= -273 --Greater then or equal to absolute zero.
  16.         do
  17.             -- Create a temperature object encapsulating value 'v' intended in Celsius.
  18.             celsius := v
  19.  
  20.         ensure
  21.             temperature_is_set: celsius = v
  22.         end
  23.  
  24.     make_kelvin (v: INTEGER)
  25.             -- Create with Kelvin value `v'.
  26.         require
  27.             temperature_is_valid: v >= 0  --Greater then or equal to absolute zero.
  28.         do
  29.             -- Create a temperature object encapsulating value 'v' intended in Kelvin.
  30.             Current.make_celsius (v - 273)
  31.  
  32.         ensure
  33.             temperature_is_correctly_set: celsius = v - 273
  34.         end
  35.  
  36. feature -- Access
  37.  
  38.     celsius: INTEGER
  39.             -- Value in Celsius scale.
  40.  
  41.     kelvin: INTEGER
  42.             -- Value in Kelvin scale.
  43.         do
  44.             Result := celsius + 273
  45.         end
  46.  
  47. feature -- Measurement
  48.     less_or_equal alias "<=" (other : TEMPERATURE) : BOOLEAN
  49.     require
  50.         other_not_void: other /= Void
  51.     do
  52.         Result := Current.celsius <= other.celsius
  53.     ensure
  54.             result_correct: (Result and Current.celsius <= other.celsius) or (not Result and Current.celsius > other.celsius)
  55.     end
  56.  
  57.     greater_or_equal alias ">=" (other : TEMPERATURE) : BOOLEAN
  58.     require
  59.             other_not_void: other /= Void
  60.     do
  61.         Result := Current.celsius >= other.celsius
  62.     ensure
  63.             result_correct: (Result and Current.celsius >= other.celsius) or (not Result and Current.celsius < other.celsius)
  64.     end
  65.  
  66.     less_then alias "<" (other : TEMPERATURE) : BOOLEAN
  67.     require
  68.             other_not_void: other /= Void
  69.     do
  70.         Result := Current.celsius < other.celsius
  71.     ensure
  72.             result_correct: (Result and Current.celsius < other.celsius) or (not Result and Current.celsius >= other.celsius)
  73.     end
  74.  
  75.     greater_then alias ">" (other : TEMPERATURE) : BOOLEAN
  76.     require
  77.             other_not_void: other /= Void
  78.     do
  79.         Result := Current.celsius > other.celsius
  80.     ensure
  81.             result_correct: (Result and Current.celsius > other.celsius) or (not Result and Current.celsius <= other.celsius)
  82.     end
  83.  
  84.     average (other: TEMPERATURE): TEMPERATURE
  85.             -- Average temperature between `Current' and `other'.
  86.  
  87.         require
  88.             other_not_void: other /= Void
  89.  
  90.         local
  91.             new_temperature_object : TEMPERATURE
  92.             new_temperature_value : INTEGER
  93.  
  94.         do
  95.             -- Compute the average of two temperature. One is given by the current object,
  96.             -- the other is passed as an argument.
  97.  
  98.             new_temperature_value := ((other.celsius + Current.celsius)/2 + 0.5).floor
  99.             create new_temperature_object.make_celsius(new_temperature_value)
  100.             Result := new_temperature_object
  101.         ensure
  102.             result_correct: (Result >= Current and Result <= other) or (result <= Current and result >= other)
  103.         end
  104.  
  105. invariant
  106.     temperature_is_valid: Current.kelvin >= 0
  107.  
  108. end
Advertisement
RAW Paste Data Copied
Advertisement