Re: Ada Interfaces and the Liskov Substitution Principle

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Tue, 29 May 2007 22:46:12 +0200, Georg Bauhaus wrote:

> 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?

Why are you sure that your daily work isn't based on such models? You could
use them unconsciously.

>> 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. 

Come on, embedded controllers operate the valves and ignition of the motor
right now. Be sure burning is a lot faster than steering / braking.

But that is not the point. The point one is - how would you enjoy the
"spinal programming" model of things you do care? The second point is - why
to program anything we don't care?

>>> 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?

Yes, as you don't mention the operation of.

>>> 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?

That k is a pair of functions mapping the system state to the value of k
and reverse:

   Get_k : S -> Integer
   Set_k : S x Integer -> S 

Thank you for making my point! What mathematics makes here is all the rest,
which could well be incomputable. Consider k a hardware random generator.
You could not describe it in any programming language, but you can in the
language of probability theory.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de