From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.swapon.de!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: A function that cannot be called? Date: Sun, 21 Oct 2018 13:57:26 +0300 Organization: Tidorum Ltd Message-ID: References: <7ab688d0-b6b8-459c-b5b7-39b6c35daad2@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Trace: individual.net SLk8PDQuJGE0MAQAJU2QVw+EQXoxY1CVbtU7wmWlNwUUOQMZhT Cancel-Lock: sha1:LcdRn5OpYnrLVmVO4hruqQrP3sI= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 In-Reply-To: Xref: reader02.eternal-september.org comp.lang.ada:54680 Date: 2018-10-21T13:57:26+03:00 List-Id: On 18-10-21 12:07 , G.B. wrote: > On 20.10.18 13:13, Simon Wright wrote: >> "G.B." 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 . @ .