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=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,2ff5c149712ec0eb X-Google-Attributes: gid103376,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news3.google.com!proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Tue, 29 May 2007 22:46:12 +0200 From: Georg Bauhaus Organization: elsewhere User-Agent: Thunderbird 1.5.0.10 (Macintosh/20070221) MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Ada Interfaces and the Liskov Substitution Principle References: <1179953657.839272.160320@a26g2000pre.googlegroups.com> <1179991769.376381.252010@m36g2000hse.googlegroups.com> <12h6mi42jcha0.7f9vfsnihjwr$.dlg@40tude.net> <1180003336.1163.29.camel@kartoffel> <83abvs7sa9.fsf@hod.lan.m-e-leypold.de> <465aa5ba$0$23147$9b4e6d93@newsspool1.arcor-online.net> <465b6606$0$10188$9b4e6d93@newsspool4.arcor-online.net> <1180445634.5664.23.camel@kartoffel> <39viqigjwhrb$.gz67xvpinyjr.dlg@40tude.net> In-Reply-To: <39viqigjwhrb$.gz67xvpinyjr.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: <465c9077$0$23135$9b4e6d93@newsspool1.arcor-online.net> NNTP-Posting-Date: 29 May 2007 22:43:35 CEST NNTP-Posting-Host: 34f945e8.newsspool1.arcor-online.net X-Trace: DXC=MTQTF=aPg[m016@cHD@m;jic==]BZ:afn4Fo<]lROoRaFl8W>\BH3YbZ7ndf4S17[eA:ho7QcPOVc@UNj]R0J^_f7VU4YdjUJ`f X-Complaints-To: usenet-abuse@arcor.de Xref: g2news1.google.com comp.lang.ada:15972 Date: 2007-05-29T22:43:35+02:00 List-Id: 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? :-)