Re: A function that cannot be called?

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 18-10-21 12:07 , G.B. wrote:
> On 20.10.18 13:13, Simon Wright wrote:
>> "G.B." <bauhaus@notmyhomepage.invalid> writes:
>>
>>> It might wet your appetite to recall that without the formal model
>>> of classical logic, none of Ada or its RM would be used by us.
>>
>> *whet
> (Ah. Thank you.)
>> Who is "us"? Certainly doesn't include me.
>
> The idea is that classical logic caused, and continues to cause,
> (features of) programming languages like Ada, in some sense.
> The idea is not to suggest that programmers need to be concerned
> with formal models in order to write programs.
>
> So, I guess for writing an embedded program like
>
>   loop
>     Ouput (Compute (Input));
>   end loop;
>
> one doesn't need to be aware that classical logic, without some
> type system, incurs the possibility of the HALTing trouble.

IMO most of the logicians' worry about the non-termination of such 
"embedded" programs is a red herring and of no importance.

The logical view of an embedded program with an outermost eternal loop, 
as above, should consider a single cycle, that is, a program like this:

    assume Cycle_Invariant (State);
    read Inputs;
    compute Outputs from Inputs and State;
    write Outputs;
    update State to New_State;
    assert Cycle_Invariant (New_State);

which has no non-termination aspects related to the cyclic loop.

If the logical model has to consider some coupling of the Outputs of one 
cycle to the Inputs of the next cycle (for control-loop stability 
analysis, say) the State can often be extended to cover that coupling.

Things become more complicated when the program contains cyclic tasks 
with various periods and perhaps some sporadic tasks. But it seems to me 
that such a complex multi-task program should divide its state into 
concurrent parts, anyway, and the invariants describing the validity of 
those state parts, and perhaps their mutual validity too, should be 
robust against all the task interleavings that can occur during 
execution. The logical model of even the longest-cycle task needs to 
consider only a statically bounded number of executions of the 
higher-rate or sporadic tasks, so the logical models of all tasks can 
assume that the outermost "non-terminating" loop, in any task, repeats 
for a statically bounded number of times.

That said, I certainly consider termination analysis to be an important 
subject. But I am more interested in _quantitative_ termination bounds 
(for WCET analysis) than in yes/no analysis.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .