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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 Path: border1.nntp.dca3.giganews.com!border2.nntp.dca3.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!news.bbs-scene.org!de-l.enfer-du-nord.net!feeder1.enfer-du-nord.net!cs.uu.nl!news.stack.nl!aioe.org!.POSTED!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: Seeking for papers about tagged types vs access to subprograms Date: Mon, 06 May 2013 17:15:36 +0200 Organization: Ada @ Home Message-ID: References: <17ceq51ydy3s0.s94miqqzbg5w.dlg@40tude.net> <1vrhb7oc4qbob$.q02vuouyovp5$.dlg@40tude.net> NNTP-Posting-Host: 01/BPNoqk8s7XmPzrYdoUA.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable X-Complaints-To: abuse@aioe.org User-Agent: Opera Mail/12.15 (Linux) X-Notice: Filtered by postfilter v. 0.8.2 X-Original-Bytes: 6115 Xref: number.nntp.dca.giganews.com comp.lang.ada:181450 Date: 2013-05-06T17:15:36+02:00 List-Id: Le Mon, 06 May 2013 16:16:02 +0200, Dmitry A. Kazakov = a =C3=A9crit: >> Theoretically. In practice, GNAT don't agree (*). It has a pragma for= >> that, `pragma Restrictions (No_Dispatching_Calls)` which should even >> enforce it in a whole application, but seems even with this active, i= t >> still requires the whole part of the runtime dedicated to it, a part = = >> which >> depends on this part, > > I suppose it would be difficult to implement this so that the code use= d = > to > maintain dispatching tables and tags could be removed. It may require = two > versions of the compiler. Furthermore there are packages defining > operations on tags which could require some of the stuff. > > Why do you bother? Especially, because dispatching calls are = > deterministic > and could be done time bounded, unless you manipulate tags. (Not = > everything > in people write in their guidelines for RT projects makes sense.) That's not real=E2=80=91time, that's just saving dependencies (have to b= e static) = and memory (static linking easily make it big) and to be sure to know = what's running beneath (no implicit heap allocation, no secondary stack,= = bounded stack, no output to standard I/O streams except if the program d= o = it explicitly, and so on). Initially I just wanted to get ride of functi= on = returning unconstrained types and the exceptions runtime (I don't like = exceptions used to return the status of an operation anyway) and keep on= ly = the last=E2=80=91chance handler, but it appears the high level parts of = the = runtime depends on the exceptions support (ex. direct or indirect = dependencies to Ada.Exceptions and al.). There is surely a way to get ri= de = of exceptions without loosing all of the rest in the while, but I don't = = want to spend time diving in the runtime nor want to make uncertain/unsa= fe = modifications, I have something else to do which can be done without = tagging types (at the cost of some useful facilities like = initialization/finalization). >> However and in the large, I >> agree with you and share the same understanding of the topic, at leas= t >> theoretically. > > There are far reaching consequences of having classes for all types. Interfaces for all types :-D >> (*) Don't know if SPARK agree and believe something can be proved abo= ut >> such a system, it's a too long time I didn't use it. A quick search o= n = >> the >> web seems to show it may be possible. > > Yes, through global analysis. Though I would prefer a much finer appro= ach > when time constraints could be imposed on the interface rather than = > checked afterwards. SPARK is often said to be used for application with time and memory boun= ds = requirement, but I don't know any way to prove timing bounds in SPARK. > What is in the interface cannot be decided before you have > interfaces properly articulated. Thus type system overhaul is the firs= t > step to make. Saying =E2=80=9Coverhaul=E2=80=9D, you will always get this reply: =E2=80= =9Cno way, don't break = compatibility=E2=80=9D (something which in the meanwhile is easily under= stood). = May be there would be a hope to do something similar to what SPARK did, = = just with bigger consequences, re=E2=80=91factoring Ada outside of Ada (= which is = unavoidable to go ahead without fears to break compatibility). > Without doing that you get only mess. > See Ada 2012 dynamic > pre-/postconditions as an example. I did not encountered any real mess so far with dynamic pre/post = condition. The only grief I have with it, is that it makes no distinctio= n = between sub=E2=80=91program used for pre/post conditions and sub=E2=80=91= programs used for = the program. Occasionally, that may lead to contradictions or impossible= = design. I would like a way to permit to restrict some sub=E2=80=91progra= ms for use = with pre/post conditions only and disallow their use from the program = proper (just like you have to separate meta=E2=80=91language and object=E2= =80=91language, = even when both shares the same vocabulary and grammar). At least, and = external language like SPARK annotations is, does not suffers from this = = confusion: a predicate may be expressed in terms of Ada entities, but is= = not imposed to be entirely expressed in these terms and never injects = anything into the program (sorry for digressing (red=E2=80=91face)). -- = =E2=80=9CSyntactic sugar causes cancer of the semi-colons.=E2=80=9D [1] =E2=80=9CStructured Programming supports the law of the excluded muddle.= =E2=80=9D [1] [1]: Epigrams on Programming =E2=80=94 Alan J. =E2=80=94 P. Yale Univers= ity