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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.swapon.de!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: Quick question regarding limited type return syntax Date: Mon, 04 Aug 2014 22:37:27 +0300 Organization: Tidorum Ltd Message-ID: References: <166aaec5-5e9c-40e0-9b07-9b9c7d5f7f33@googlegroups.com> <16a6846f-2964-438a-ab9b-2029075f7924@googlegroups.com> <20m59uxjlygw$.2mpabkt469vp.dlg@40tude.net> <1ge2ly0v5yk8d.j8pd98xg0o8v.dlg@40tude.net> Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: individual.net ueWo4uReNDgRAKRDzr2Q2gfluLqMnhxA9CMDqLKPaAGkcQvugR Cancel-Lock: sha1:41wL6BdyhPaJlcT2qCPAfndiH6s= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:24.0) Gecko/20100101 Thunderbird/24.6.0 In-Reply-To: <1ge2ly0v5yk8d.j8pd98xg0o8v.dlg@40tude.net> Xref: news.eternal-september.org comp.lang.ada:21451 Date: 2014-08-04T22:37:27+03:00 List-Id: On 14-08-04 15:43 , Dmitry A. Kazakov wrote: > On Mon, 04 Aug 2014 12:24:19 +0300, Niklas Holsti wrote: > >> Controlled types in Ada provide hooks (Initialize/Finalize/Adjust) that >> can be used as constructors and destructors, > > Not really. Ok, I should have said "for similar purposes as constructors and destructors". > The problem is that they hook too late to be specific type > constructor and too early for a specific type destructor. This is why you > can dispatch from there. The problem arise when you attempt both: use > Initialize as if it were a specific constructor hook and dispatch from it. You have a certain concept of what a "constructor" should do, and should not do; the latter includes dispatching. Ada allows dispatching from Initialize, but you can disallow it by a personal design and coding rule. >> I don't agree that dispatching on a controlled object should be illegal >> until the Initialize operation on that object has been completed. > > Then you cannot call Initialize a constructor's hook. Depends on the meaning you assign to "constructor". In Ada, the object is created and default-initialized (or initialized by component-specific Initialize calls) before Initialize is called on it. In this sense, construction in Ada is automatic, and Initialize is only a "post-constructor" hook. > To make it clearer consider what would be the post-condition of Initialize: > > type T is ...; > type S is new T ...; > > Initialize (X : in out T) > ensure > T'Operational (X) > > [*] or, maybe > > S'Operational (X) > T'Class'Operational (X) > S'Class'Operational (X) You have invented a boolean predicate "Operational". In practice, objects do not have only two states: "not operational" and "operational"; they have several states, and "initialization" is often a multi-step process which takes the object through a sequence of logical states, from its default-initialized state to whatever level of initialization is desired at this stage. For a well-worn example, a File object is usually born in a "closed" state, and is then "operational" only in a limited sense; later, opening the File makes it more "operational". Some steps in the initialization process, while described in the semantics of the parent type (the 'Class), may need assistance that is specific to a derived type, and therefore dispatching from Initialize may be useful. For example, the 'Class semantics may include registration of all objects in some registry, but this registry may need some object-specific data that depends on the particular type of the object and is provided by a dispatching operation. > Now, the precondition of a dispatching call on T'Class is obviously: > > require > T'Class'Is_Operational (X) > > Of course: > > T'Class'Operational (X) => T'Operational (X) > T'Class'Operational (X) => S'Operational (X) > > From this you can formally analyse if initialization is correct. Only in your limited, two-state formalization, which IMO is not realistic. >> Moreover, I think this question of constructor/destructor control flow >> is separate from the general question of preventing access to >> uninitialized data. > > ? Initialization = construction. I don't see how are they different. The point is that for some data structures, it is not desirable to initialize (= store data in) all allocated storage locations when the data structure is created. The reason can be that initialization is too costly, and the initialization values are never used; or the reason can be that the initialization could only assign dummy values, and therefore would only ensure that later errors have a deterministic effect, but could not ensure that no dummy initial values are used by mistake as non-dummy values. The canonical example is a large array that will be used as a stack, or in which data blocks will be allocated and deallocated in some other controlled way. Thus, the array is created (i.e. allocated or constructed) but usually it still contains uninitialized and therefore unpredictable data (at least in traditional processors and operating systems -- some new or security-conscious systems have memory allocators which do initialize all allocated memory areas, albeit with dummy values such as zeros). Such data structures usually have special components which "indicate" which parts of the data structure are initialized and usable, and which parts are not. For example, a stack pointer can perform this role for an array that implements a stack. But current programming languages, including Ada, do not provide any general support for this logical connection between "indicators" and initialized/uninitialized data; the connection must in each case be specifically formalized and then used to prove that any data that is read has first been initialized (with real values). My aim was to complain about this lack of language support for such "indicators" and other features that help to prove that a program never uses uninitialized variables (nor dummy values). I don't know what form this support should take, however. As a partial analogy, discriminant checks for variant records in Ada ensure that non-existent components are not accessed, but do not ensure that the accessed components are initialized with useful values. -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .