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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,7b207d193114a9,start X-Google-Attributes: gid103376,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!postnews.google.com!e10g2000prf.googlegroups.com!not-for-mail From: Eric Hughes Newsgroups: comp.lang.ada Subject: Partial type specifications and their ordering Date: Mon, 17 Mar 2008 16:14:42 -0700 (PDT) Organization: http://groups.google.com Message-ID: NNTP-Posting-Host: 166.70.57.218 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: posting.google.com 1205795683 25771 127.0.0.1 (17 Mar 2008 23:14:43 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 17 Mar 2008 23:14:43 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: e10g2000prf.googlegroups.com; posting-host=166.70.57.218; posting-account=5RIiTwoAAACt_Eu87gmPAJMoMTeMz-rn User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.8.1.12) Gecko/20080201 Firefox/2.0.0.12,gzip(gfe),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:20459 Date: 2008-03-17T16:14:42-07:00 List-Id: My comment earlier today got my mind in a buzz on the topic of partial types, so as a form of personal exorcism I wrote a skeleton draft. I first came upon this idea which thinking about types from a program correctness point of view, so I've included all that as well; it's even relevant, though not immediately obvious. I'm not sure I got quite all of the details right; corrections welcome. A partial type is a collection of zero or more of each the following: A. Generic formal parameters 1. formal objects, specified as satisfying some partial type. 2. formal partial types 3. formal partial subprograms 4. formal partial packages B. Partial discriminants, that is, a discriminant specified with partial types C. Partial subprograms, that is, subprograms specified with partial types D. Partial record components, objects specified with partial types For two partial types T1 and T2, we say that T1 < T2 if all the following hold. If so, then we also say that T1 satisfies T2. Colloquially T1 is a subtype of T2 and T2 is a supertype of T1. I. Language relationships A. The generic parameters of T2 are a subset of those of T1. B. The discriminants of T2 are a subset of those of T1. C. The subprogram names of T2 are a subset of those of T1. D. For each subprogram name F in T2 1. the number of parameters of F in T1 and T2 are equal, and 2. the names of parameters of F in T1 and T2 are pairwise equal, and 3. the partial type of a parameter in T2 is a supertype of the corresponding parameter in T1, and 4. the return value of T2 is a subtype of the return value of T1 E. For each component name C in T2 1. there is a component named C in T1, and 2. the partial type of T1.C is a subtype of T2.C II. Predicate relationships A. The instantiation conditions on the generic parameters of T1 imply those of T2. B. The instantiation conditions on the discriminants of T1 imply those of T2. C. For each subprogram name F in T2 1. the preconditions of T1.F imply those of T2.F, and 2. the postconditions of T2.F imply those of T1.F D. The invariants of T1 imply those of T2. Each ordinary type has a canonical partial type associated with it. For a tagged type U, the canonical partial type of a subtype of U satisfies the canonical partial type of U. The canonical partial type of limited view of a type U satisfies the canonical partial type of U. The reason the predicate relationships are in there is to be able to reason about limited types. Limited types can be seen as having required postconditions of the form "in C = out C", that is, no component is modified by a subprogram. Some theorems: "<" on partial types is a partial ordering. The set of partial types with "<" is a lattice. The lattice is upper-bounded by the nil type. Whew. Enough for now. Eric