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!newsfeed.gamma.ru!Gamma.RU!newsfeed.icl.net!newsfeed.fjserv.net!colt.net!feeder.news-service.com!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail Newsgroups: comp.lang.ada Subject: Re: Ada Interfaces and the Liskov Substitution Principle From: Georg Bauhaus In-Reply-To: <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> <465c9077$0$23135$9b4e6d93@newsspool1.arcor-online.net> Content-Type: text/plain Content-Transfer-Encoding: 7bit Message-Id: <1180531107.16197.30.camel@kartoffel> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Date: Wed, 30 May 2007 15:18:27 +0200 Organization: Arcor NNTP-Posting-Date: 30 May 2007 15:18:25 CEST NNTP-Posting-Host: edde2eee.newsspool2.arcor-online.net X-Trace: DXC=__CWdT3^DiI2:OR3:3gaE@A9EHlD;3YcB4Fo<]lROoRA8kF On Wed, 2007-05-30 at 09:53 +0200, Dmitry A. Kazakov wrote: > > 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. Hm. If you are suggesting that we have a working model of unconscious mathematics, then in a sense, empirical programming science would try to observe its working patterns then. > 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? I'm assuming programmers who work carefully. Let them be guided by principles. The principles need not be the best thing since sliced bread only because they have been described standard math terms. > >>> 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. I mean, what mathematical model (such as LSP) is helpful in describing this particular loop, such that the math of the model rules out writing k := k + 1; for example? I would start with a model that isn't originally inspired by mathematics (because higher math typically frowns upon operations, that is, the things that computers do). My vague model has loop invariants, loop termination, and the fact that the type Integer happens to include a successor function in its interface. Now, the type Integer offers much more than that, e.g. "*". Still, it seems reasonable to start from the mathematical structure that maps to a type like Integer, even when I do not need either of the inverse, the neutral element, or commutativity, which Integer types have (mostly), among other things. > >>> 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 That's not a mathematical model. It is a pair of functions that can be mapped to some aspects of how k is supposedly operating, when amended with sequencing. I bet that few programmers writing the above loop will have functions in mind that map from and to world state. > 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. Thank you for making my point! :-) Probability theoretic constructs can be mapped into executable computer constructs only in very limited ways, some of them using clever bit shuffling, others relying on something *outside* the reach of mathematics, such as /dev/random (as opposed to /dev/urandom). Outside insofar as there is no practical way of mapping noise to a precise, hence programmable, formula. This doesn't make them any less useful.