mirror of
https://github.com/AdaCore/spark2014.git
synced 2026-02-12 12:39:11 -08:00
24 lines
484 B
Ada
24 lines
484 B
Ada
package Indicator
|
|
--# own out Outputs : Settings;
|
|
is
|
|
--# type Settings is abstract;
|
|
function IsOn return Boolean;
|
|
|
|
procedure TurnOn
|
|
with Post => (IsOn);
|
|
--# global out Outputs;
|
|
--# derives Outputs from ;
|
|
--# post IsOn (Outputs);
|
|
--
|
|
-- Turns the indicator on.
|
|
|
|
procedure TurnOff
|
|
with Post => (not IsOn);
|
|
--# global out Outputs;
|
|
--# derives Outputs from ;
|
|
--# post not IsOn (Outputs);
|
|
--
|
|
-- Turns the indicator off.
|
|
|
|
end Indicator;
|