SPARK modeling the passage of time

SPARK modeling the passage of time

[Maciej Sobczak]

Consider a system that has one digital input and one output and the requirement saying that the output should be set True when the input is True, but the Output should stay True for at least 5 seconds, even if Input goes off sooner.
In other words, the following sequence is OK (each step is one second):

 Input: 0 0 1 0 0 0 0 0 0 1 1 1 1 1 1 1 0 ...
Output: 0 0 1 1 1 1 1 0 0 1 1 1 1 1 1 1 0 ...

Note that Output is set to True as soon as Input is detected to be True, but the Output stays True for at least 5 steps.

I have managed to model the dependencies between input, output and some abstract state (the system obviously has memory) like this:

pragma SPARK_Mode;

package Signals
    with Abstract_State => State,
         Initializes => State
is

    procedure Process (Input : in Boolean; Output : out Boolean)
        with Global => (In_Out => State),
             Depends => (State => (Input, State),
                         Output => (Input, State));

end Signals;

(the assumption is that the Process procedure is called in equal intervals, so that we don't need a dedicated clock to manage the passage of time)

I was also able to actually implement it like here:

pragma SPARK_Mode;

package body Signals
    with Refined_State => (State => (Counter, Last_Output))
is

    Time_Off : constant := 5;
    Counter : Natural := 0;
    Last_Output : Boolean := False;

    procedure Process (Input : in Boolean; Output : out Boolean)
        with Refined_Global => (In_Out => (Counter, Last_Output)),
             Refined_Depends => (Counter => (Input, Last_Output, Counter),
                                 Output => (Input, Last_Output, Counter),
                                 Last_Output => (Input, Last_Output, Counter))
    is
    begin
        if not Last_Output and Input then
            Counter := Time_Off;
        end if;

        Output := Input or (Counter > 0);
        Last_Output := Output;
        
        if Counter > 0 then
            Counter := Counter - 1;
        end if;
    end Process;

end Signals;

If Process is called repeatedly with varying Input, the Output will be set and retained between calls as expected.

The problem is: the spec has no functional contract, only dependency constraints. The functional contract (presumably in terms of a Post-condition) should somehow define the dependency between consecutive calls and the abstract state is not enough to express the whole requirement.

Have you done something like this in SPARK already and do you have some hints on how this can be achieved?

-- 
Maciej Sobczak * http://www.inspirel.com/

Re: SPARK modeling the passage of time

[phil.clayton]

Only just saw this post.  Good question!

Standing back from your problem, what you are finding is that pre- and postconditions aren't the most general form of specification.  They are conditions on the state of a program at a particular position in the program, perhaps relative to another position.  They define a simple contract: if the precondition holds before a program, then the postcondition holds after the program.  And therein lies the fundamental limitation: a postcondition is required to hold only _after_ the program has terminated.  A postcondition cannot specify the behaviour of a program that does not terminate because the postcondition is never required to hold [3].  Pre- and postconditions really are for terminating programs.  Unfortunately, a major class of non-terminating program is control systems, like your example.


On Tuesday, 3 March 2015 15:47:43 UTC, Maciej Sobczak  wrote:
> Consider a system that has one digital input and one output and the requirement saying that the output should be set True when the input is True, but the Output should stay True for at least 5 seconds, even if Input goes off sooner.
> In other words, the following sequence is OK (each step is one second):
> 
>  Input: 0 0 1 0 0 0 0 0 0 1 1 1 1 1 1 1 0 ...
> Output: 0 0 1 1 1 1 1 0 0 1 1 1 1 1 1 1 0 ...
> 
> Note that Output is set to True as soon as Input is detected to be True, but the Output stays True for at least 5 steps.

This is what a control engineer might call a Minimum Pulse Delay or Minimum Drive Pulse.


> I have managed to model the dependencies between input, output and some abstract state (the system obviously has memory) like this:
> 
> pragma SPARK_Mode;
> 
> package Signals
>     with Abstract_State => State,
>          Initializes => State
> is
> 
>     procedure Process (Input : in Boolean; Output : out Boolean)
>         with Global => (In_Out => State),
>              Depends => (State => (Input, State),
>                          Output => (Input, State));
> 
> end Signals;
> 
> (the assumption is that the Process procedure is called in equal intervals, so that we don't need a dedicated clock to manage the passage of time)
> 
> I was also able to actually implement it like here:
> 
> pragma SPARK_Mode;
> 
> package body Signals
>     with Refined_State => (State => (Counter, Last_Output))
> is
> 
>     Time_Off : constant := 5;
>     Counter : Natural := 0;
>     Last_Output : Boolean := False;
> 
>     procedure Process (Input : in Boolean; Output : out Boolean)
>         with Refined_Global => (In_Out => (Counter, Last_Output)),
>              Refined_Depends => (Counter => (Input, Last_Output, Counter),
>                                  Output => (Input, Last_Output, Counter),
>                                  Last_Output => (Input, Last_Output, Counter))
>     is
>     begin
>         if not Last_Output and Input then
>             Counter := Time_Off;
>         end if;
> 
>         Output := Input or (Counter > 0);
>         Last_Output := Output;
>         
>         if Counter > 0 then
>             Counter := Counter - 1;
>         end if;
>     end Process;
> 
> end Signals;
> 
> If Process is called repeatedly with varying Input, the Output will be set and retained between calls as expected.
> 
> The problem is: the spec has no functional contract, only dependency constraints. The functional contract (presumably in terms of a Post-condition) should somehow define the dependency between consecutive calls and the abstract state is not enough to express the whole requirement.
> 
> Have you done something like this in SPARK already and do you have some hints on how this can be achieved?

I haven't done this with the SPARK Examiner but have done this using a static analysis tool called ProofPower/DAZ.  The general concepts are the same.

In very simple terms, a digital control system samples inputs and recalculates outputs by periodically performing the same function.  The basic form of implementation is a 'while' loop as follows:

  Init;             -- initialize state
  while true
  loop
    Step;           -- calculate outputs and update state
    ...             -- any other stuff
    delay ...;      -- wait until end of sampling period
  end loop;

For reasons given above, a postcondition for the whole program is of no use.  Therefore, pre- and postconditions are only able to specify the behaviour of a single step, i.e. the loop body, as follows:

  Init;             -- initialize state
  while true
  loop
    { pre }
    Step;           -- calculate outputs and update state
    ...             -- any other stuff
    delay ...;      -- wait until end of sampling period
    { pre ∧ post }  -- [1]
  end loop;

You need a separate higher-level argument to justify the overall behaviour against some specification [2].

In some digital control systems, there may not be a loop statement in code.  For example, a hardware function may be used to restart each iteration.  In that case, the body is analysed in isolation:

  { pre }
  Step;           -- calculate outputs and update state
  ...             -- any other stuff
  delay ...;      -- wait until end of sampling period
  { pre ∧ post }

post should contain the overall postcondition for a single iteration of the loop body.  This would be an aggregation of the postconditions of the individual parts, including Step.
pre would capture any invariant conditions that need to be assumed, and therefore maintained.

It may be tempting to place the pre- and postcondition around the Step subprogram only as follows:

  { pre }
  Step;           -- calculate outputs and update state
  { pre ∧ post }  -- NOT HERE!
  ...             -- any other stuff
  delay ...;      -- wait until end of sampling period

This does not check that "any other stuff" does not change variables that Step expects to persist from one iteration to the next.  

The postcondition of Step would describe its function for a single execution.  How you derive this depends on what you are trying to achieve.  You could just work up from the code but the code would obviously meet that postcondition whether right or wrong.  You could work down from the overall specification in [2], assuming nothing about the code, by converting it to a single-step specification.

Any internal state that Step depends on must be mentioned in its postcondition to justify against the overall specification [2].  That may require package body variables to be brought up to the package specification level (using own/Abstract_State), which you have done.  I expect you'll need to introduce proof/ghost functions to refer to properties of it in postconditions, however.  Have you looked at:
http://docs.adacore.com/spark2014-docs/html/lrm/mapping-spec.html#quoting-an-own-variable-in-a-contract
?

I note that your function Process is not 'reusable'.  In control system software, it would much more common for a library subprogram to have state as an 'in out' parameter so that it can be reused in different instances, e.g.

  procedure Process
   (Input  : in     Boolean;
    State  : in out Process_State;
    Output :    out Boolean)

Doing this would avoid the need to expose internal state variables.

Regards,

Phil


[1] At the end of the loop body, control always flows back to the start of the body.  Therefore we must check that
  pre ∧ post ⇒ pre
This is trivially so because we have included pre in the postcondition of the loop body.

[2] For example:

  out n ⇔ in n ∨ (out (n - 1) ∧ ∃ n' : n - 5/dt .. n - 1 ⦁ ¬ out n')

"The output is true on step n if and only if either the input is true on step n or the output was true on step n - 1 and there exists a step in the previous 5 seconds when the output was not true."

[3] With some static analysis tools, a postcondition of false can be used to show that a program does not terminate because false is unachievable so the tool will be showing a path to false is not possible.  Of course, a condition that is false cannot say anything else.

Re: SPARK modeling the passage of time

[Maciej Sobczak]

> Only just saw this post.  Good question!
> [...]

Thank you Phil, this gives me some food for further experiments. The idea of extracting the (implicit) state to something that becomes an in/out parameter of the step function is an interesting idea, as it allows us to be more explicit with regard to how the history of invocations is maintained.
I think I got lost because I tried to encapsulate the state and by doing this I lost the means to express the specification. If we treat the history of invocations as something visible at the place of specification (like an in/out parameter of some array type, for example), then the rest seems much easier.

> [2] For example:
> 
>   out n ⇔ in n ∨ (out (n - 1) ∧ ∃ n' : n - 5/dt .. n - 1 ⦁ ¬ out n')

-- 
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com