Re: Ada Interfaces and the Liskov Substitution Principle

[Georg Bauhaus <bauhaus@futureapps.de>]

Dmitry A. Kazakov wrote:
>  This is all
> programming is about - porting mathematics. (:-)) To model the reality in
> just one hop might be just impossible for a normal programmer. You cannot
> rely on Nobel Price laureates, they are rare, expensive and uninterested in
> our problems.

OK. So why should a normal programmer like me consider it a cost effective
idea to try to construct a proven mathematical model for my daily work?
I do sometimes run Prolog or SETL to help me with higher level
specifications and find this quite helpful. OTOH, in these cases I am
drawing upon models that are different from, say, LSP. They are more like
general purpose mathematical building blocks. LSP is a formal
and well defined whole. Arguably, it isn't a good model from some points of
view, even though there is "mathematics" in it which, you say, programming
will port to a program.



>> Many programs just happen to be a model of reality, and they still
>> work well, even though they were not mathematically designed.
>> The programmers are hardly aware of every conceivable mathematical
>> property of their model. Still, they write sound programs.
> 
> How can you know that? (:-)) Let's take the braking control system for your
> next car...

I hear that Mercedes engineers do not yet want to replace
the steering wheel with a embedded computer joy stick thing ... :-)
I think the argument is that a car must make quicker moves in more
constraining environments than your average airliner. 



>> What I want is the mathematics of program models, more than programming
>> to satisfy mathematics. BTW, what is the best suited mathematical
>> structure that (minimally) describes the loop
>>
>>    while k < 100 loop
>>      k := Integer'succ(k);
>>    end loop;
> 
> Ordered set, mathematical induction etc.

Uhm, can we have less than a group?


>> and how does it help?
> 
> A lot. For example it can tell the code reviewer that the above program is
> equivalent to:
> 
>     if k < 100 then
>       k := 100;
>    end if;

Making assumptions about k ... This is how mathematics can make us prefer
default perspectives by moving all important points of view behind Formal
Mountains. The above change wouldn't have helped at all, on the contrary,

   for k'Address use ...;

What's the mathematics of that, then?

:-)