Operation can be dispatching in only one type
in [ADA]
|
From: Dmitry A. Kazakov on 2 Dec 2009 04:07 On Wed, 02 Dec 2009 02:13:14 +0100, Georg Bauhaus wrote: > On 12/1/09 7:47 PM, Dmitry A. Kazakov wrote: > >> It cannot be declared of Car, if it is not. > > Which brings us (or me, at least) to the problem of whether or > not the meaning of an Ada program (or a sequential subprogram) > will change if object X really "is" after "begin" or whether > its physical existence is allowed start just before actual > use. :-) X might show its existence through side effects > of its default initialization. > Rather implicit if the effect is important. Ada rules are rather complex, the object exists right after its declaration, but its existence is somewhat sleepy, a larva, not yet the butterfly: Consider the following: task type A is entry Hey; end A; type T (Greeting : access A) is new Ada.Finalization.Limited_Controlled with null record; overriding procedure Initialize (X : in out T); task body A is begin accept Hey; end A; procedure Initialize (X : in out T) is begin X.Greeting.Hey; end Initialize; With the above: declare X : aliased A; Y : T (X'Access); -- This is a deadlock! begin The object X (a task) is not completely initialized when Y's Initialize is called. This is one of nasty problems with tasks as objects. And in general I think that many feel uncomfortable with Ada declarations being executable. I have no clear idea how to approach this problem, though. >>> There is no way to perform an operation involving X in >>> its own declaration. >> >> But it can be used right after the declaration. > > Sure, but it isn't used, and the compiler will make sure > it isn't unless it has a value. That erodes the concept of scope, which idea is that the object is usable anywhere within its scope. >> Ada does not specify what happens with out parameters updated before an >> exception gets raised in the body of Foo: >> >> procedure Foo (X : out Car) is >> begin >> if HALT (p) then >> raise Baz; -- Is this legal? >> else >> X := Merzedes; >> end if; >> end Foo; > > If we were to integrate exceptions into normal control > flow like Java does? Contracted exceptions is a way to move the check down the code. Consider an invalid initial value, which is legal. Its validness is rather determined by outcome of some operations, e.g. reading it causes Constraint_Error. Then, with exception contracts, if you declared the program as not raising Constraint_Error, then the program with an invalid initial value could become illegal if Constraint_Error is not caught: declare raise no Constraint_Error; -- Imaginary syntax X : Car; begin Print (X.Tire); end; -- Illegal, this block might rise Constraint_Error declare raise no Constraint_Error; X : Valid_Car; -- Illegal require initialization by a valid value begin Print (X.Tire); end; -- Legal now, but fails at the declaration point declare raise no Constraint_Error; X : Valid_Car := My_Car; -- A valid value begin Print (X.Tire); end; -- No Constraint_Error >> Of course there is something to catch. The compiler has to do this. So the >> question is at which cost, how many false positives and negatives it will >> find? How scalable is this feature for more elaborated types? > > From the Java point of view, there are no false positives > or negatives. Of course there are, because it is a halting problem. So you need some optimistic or pessimistic estimation of: if False then Print (X.Tire); -- Is this illegal? If yes, that is a false positive end if; [Also see Randy's points] >> My example illustrated a situation where an >> uninitialized value might be an advantage, because one possible outcome of >> Foo is exception propagation, in which case leaving Result raw could save >> some vital nanoseconds of execution time. I don't buy this. > > Whether the out mode variable had been initialized in the > body or not, the exceptional situation might have destroyed > the value of the out mode parameter. A variable would not > be considered initialized, I'd think, in an exception handler, > unless the programmer says so (or assigns a value). No the problem is whether to treat a call to the body as legal. The problem is that you could not rely on its contract (out Car), in order to be able to decide whether this call would "initialize" the object. BTW, you consider ":=" as an initialization, but why? Where is a guaranty that it initializes the object by a "valid" value? I feel that very concept is somewhat inconsistent with ADT. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: John B. Matthews on 2 Dec 2009 06:18 In article <4b15b59b$0$7632$9b4e6d93(a)newsspool1.arcor-online.net>, Georg Bauhaus <rm-host.bauhaus(a)maps.futureapps.de> wrote: [...] > The Java rule I had been thinking of starts from less emphasis on > what the default initial (Ada) value of a (local) variable might be, > given current Ada rules. Rather, in the sequence of statements below > the compiler would just not accept the reference to the .Rim_Color > component of Spare. The meaning of the declaration Spare : Tire > needs to be understood as slightly changed, to exclude (or ignore) > default initialization. > > Spare : Tire; > begin > -- Here, whatever Spare is, or whichever side effects its > -- declaration may have, it is not used between > -- its declaration and the line following the if statement. > -- Therefore, we are free to think of it as something > -- or as nothing, or as something to become a Tire when > -- necessary. A virtual object, perhaps. (Otherwise, use > -- syntax to indicate that there is something important > -- going on in default init; or, for compatibility, when > -- nothing important is going on.) > > if Some_Condition then > Spare := Make_a_Tire; > end if; > Its_Color := Spare.Rim_Color; -- illegal > > > A simple rule would now be a copy of the Java rule which is > quoted below. Just assume that Spare has no value. > Just like the last line is not accepted by SPARK or > by Java (the corresponding Java source line). The warning > which some Ada compilers will issue (that Spare may not have > been assigned a value) is then turned into an error. Ah, I see. Nothing in the present Ada specification _requires_ such a warning. > As might be expected in Ada, some syntax might be in > order to say that default initialization does > provide an initial value that warrants the safe use of the > variable after the if statement (or is needed for its > side effects, but this is another story, I guess). > > Another case is when a declared variable is used in > a declaration of another variable following it, > > Spare : Tire; > Another : Tire := Spare; -- might become illegal > begin > ... > > Illegal unless it is specified that Spare does have > a valid Tire value. Or, oddly, that Another "inherits" the > unknown state of Spare WRT being initialized or not. > > This is the Java rule I had in mind. I found it thanks to the > link you have supplied: > "A Java compiler must carry out a specific conservative flow > analysis to make sure that, for every access of a local > variable or blank final field f, f is definitely assigned > before the access; otherwise a compile-time error must occur." I can see the appeal of adding such an analysis to Ada. <http://java.sun.com/docs/books/jls/third_edition/html/defAssign.html> -- John B. Matthews trashgod at gmail dot com <http://sites.google.com/site/drjohnbmatthews>
From: John B. Matthews on 2 Dec 2009 07:35 In article <1jcbtmi5rztyp$.norvlhez9i9$.dlg(a)40tude.net>, "Dmitry A. Kazakov" <mailbox(a)dmitry-kazakov.de> wrote: Georg Bauhaus wrote: > > From the Java point of view, there are no false positives > > or negatives. > > Of course there are, because it is a halting problem. So you need > some optimistic or pessimistic estimation of: > > if False then > Print (X.Tire); -- Is this illegal? If yes, that is a false positive > end if; It would be indeterminate but for doing "a specific conservative flow analysis." In the specific cases of boolean constant expressions and if statements, if (true) { spare = new Tire(); } // spare assigned if (1 == 1) { spare = new Tire(); } // spare assigned if (false) { spare = new Tire(); } // spare unassigned if (1 == 2) { spare = new Tire(); } // spare unassigned if (always()) { spare = new Tire(); } // spare unassigned static boolean always() { return true; } In particular, spare remains unassigned even though the function always() is always true. In Ada, a certain compiler may warn 'variable "N" is assigned but never read' for the following: N : Integer; if False then N := 1; end if; I'm not especially advocating applying the Java rules to Ada, but I like the warning. <http://java.sun.com/docs/books/jls/third_edition/html/defAssign.html> -- John B. Matthews trashgod at gmail dot com <http://sites.google.com/site/drjohnbmatthews>
From: Dmitry A. Kazakov on 2 Dec 2009 08:35 On Wed, 02 Dec 2009 07:35:39 -0500, John B. Matthews wrote: > In article <1jcbtmi5rztyp$.norvlhez9i9$.dlg(a)40tude.net>, > "Dmitry A. Kazakov" <mailbox(a)dmitry-kazakov.de> wrote: > > Georg Bauhaus wrote: > >>> From the Java point of view, there are no false positives >>> or negatives. >> >> Of course there are, because it is a halting problem. So you need >> some optimistic or pessimistic estimation of: >> >> if False then >> Print (X.Tire); -- Is this illegal? If yes, that is a false positive >> end if; > > It would be indeterminate but for doing "a specific conservative flow > analysis." In the specific cases of boolean constant expressions and if > statements, > > if (true) { spare = new Tire(); } // spare assigned > if (1 == 1) { spare = new Tire(); } // spare assigned > if (false) { spare = new Tire(); } // spare unassigned > if (1 == 2) { spare = new Tire(); } // spare unassigned > if (always()) { spare = new Tire(); } // spare unassigned > > static boolean always() { return true; } > > In particular, spare remains unassigned even though the function > always() is always true. > > In Ada, a certain compiler may warn 'variable "N" is assigned but never > read' for the following: > > N : Integer; > if False then N := 1; end if; > > I'm not especially advocating applying the Java rules to Ada, but I like > the warning. Yes, warning is nice. The problem is with making it an error as Georg suggests (and Java does). An error (and its complement "no error") require much more careful definition. "Initialized" is too shaky for that, but for all I find "unassigned" inconsistent with strong typing. A typed object is always assigned because it cannot have any values other than of its type. If we wanted an object to have *certain* values, e.g. "any value different from the default one", then a naive analysis a-la Java is too little to me. I would prefer full blown pre-, postconditions and invariants for such a case. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Jean-Pierre Rosen on 2 Dec 2009 09:29
John B. Matthews a écrit : >> This is the Java rule I had in mind. I found it thanks to the >> link you have supplied: >> "A Java compiler must carry out a specific conservative flow >> analysis to make sure that, for every access of a local >> variable or blank final field f, f is definitely assigned >> before the access; otherwise a compile-time error must occur." > > I can see the appeal of adding such an analysis to Ada. > > <http://java.sun.com/docs/books/jls/third_edition/html/defAssign.html> > Unless it has changed recently (it is sometimes since I updated my Java education), the Java solution is not bullet-proof: you can still access variables before initialization from constructors. Note that if the Java people were confident in their rule, there would be no need to require that every variable be initialized to zero! -- --------------------------------------------------------- J-P. Rosen (rosen(a)adalog.fr) Visit Adalog's web site at http://www.adalog.fr |