Operation can be dispatching in only one type
in [ADA]
|
From: Dmitry A. Kazakov on 1 Dec 2009 08:37 On Tue, 1 Dec 2009 09:01:11 +0100, stefan-lucks(a)see-the.signature wrote: > BTW, I don't think initialisation and construction are actually identical, > even though they have to be performed in close temporal proximity. If > construction fails, this is a Storage_Error. No, it is Program_Error in Ada. Construction /= allocation. Here I repeat the object's life cycle as I see it: allocation construction (=initialization) use (includes assignment and all public operations) destruction (=finalization) deallocation > A failed Initialisation is > much more powerful -- it can raise any of your favourite exceptions. ;-) Well, I think it is possible to roll back an initialization, though it was not attempted in Ada. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Dmitry A. Kazakov on 1 Dec 2009 08:48 On Tue, 01 Dec 2009 13:13:29 +0100, Georg Bauhaus wrote: > Then we could rely on the language: compilers will detect > uninitialized variables provided these do not have a pragma/keyword/... > to say that uninitialized is what the programmer wants. > Some fancy means to tell the compiler that this variable > does indeed have a good first value like pragma Import. > > X : [constant] Car; -- default init, The error is here! > -- undefined, > -- junk bits. Doesn't matter > -- *no* pragma Import (Ada, X); > > begin > > Spare := X.Tire (5); -- would become illegal, Not here! ------------------------- Anyway, you cannot do that because: if HALT (P) then X := Z; end if; Y := X; -- Is this legal? > Does the phrase "first value" make sense? An object shall not have invalid values. All values are valid if the language is typed. Enforcing user-defined construction including prohibition of certain kinds of construction (e.g. per default constructor) is a different story. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Georg Bauhaus on 1 Dec 2009 10:02 Dmitry A. Kazakov schrieb: > On Tue, 01 Dec 2009 13:13:29 +0100, Georg Bauhaus wrote: > >> Then we could rely on the language: compilers will detect >> uninitialized variables provided these do not have a pragma/keyword/... >> to say that uninitialized is what the programmer wants. >> Some fancy means to tell the compiler that this variable >> does indeed have a good first value like pragma Import. >> >> X : [constant] Car; -- default init, > > The error is here! >> -- undefined, >> -- junk bits. Doesn't matter >> -- *no* pragma Import (Ada, X); >> >> begin >> >> Spare := X.Tire (5); -- would become illegal, > > Not here! Why? Nothing needs to have happened in between the X's declaration and the first reference made to it. > ------------------------- > Anyway, you cannot do that because: > > if HALT (P) then > X := Z; > end if; > Y := X; -- Is this legal? (HALT is a run-time issue that has no impact here.) While this snippet would not be legal as is (on purpose!), Ada's case coverage rules can make the programmer write a legal program easily: write an else branch! The compiler can then decide that a value will be assigned in either branch. If nothing is to be assigned this can only be for the reason that the variable is imported, or has a value already. In the former case an unchecked conversion involving only the variable will do; syntactic sugar might be nice to have. if HALT (P) then X := Z; else !X; end if; One might even omit the else branch without loss when Ada forces saying that the variable is imported. >> Does the phrase "first value" make sense? > > An object shall not have invalid values. All values are valid if the > language is typed. Enforcing user-defined construction including > prohibition of certain kinds of construction (e.g. per default constructor) > is a different story. > If you feed this to a Java compiler you will see how it is done. The Java compiler will not accept a reference to a variable's component when the variable may not have been initialized. import java.math.BigInteger; public class Dummy { enum TireColor { Black, White }; class Tire { TireColor rim_color; } public static void main(String[] args) { Tire spare; TireColor its_color; final BigInteger P; // some program's number P = BigInteger.valueOf(Long.parseLong(args[0])); if (HALT(P)) { spare = new Tire(); } // this line not accepted by a Java compiler: its_color = spare.rim_color; // <----- } static boolean HALT(BigInteger gn) { // dummy if (gn.equals(BigInteger.ZERO)) return true; return HALT(gn.add(BigInteger.ONE)); } }
From: Dmitry A. Kazakov on 1 Dec 2009 11:18 On Tue, 01 Dec 2009 16:02:21 +0100, Georg Bauhaus wrote: > Dmitry A. Kazakov schrieb: >> On Tue, 01 Dec 2009 13:13:29 +0100, Georg Bauhaus wrote: >> >>> Then we could rely on the language: compilers will detect >>> uninitialized variables provided these do not have a pragma/keyword/... >>> to say that uninitialized is what the programmer wants. >>> Some fancy means to tell the compiler that this variable >>> does indeed have a good first value like pragma Import. >>> >>> X : [constant] Car; -- default init, >> >> The error is here! >>> -- undefined, >>> -- junk bits. Doesn't matter >>> -- *no* pragma Import (Ada, X); >>> >>> begin >>> >>> Spare := X.Tire (5); -- would become illegal, >> >> Not here! > > Why? Because X is illegal right after begin: IF accessing X is illegal THEN the corresponding operation does not belong to the type of X THEN the type of X is not Car. q.e.d. (Provided, we are talking about a typed language) >> ------------------------- >> Anyway, you cannot do that because: >> >> if HALT (P) then >> X := Z; >> end if; >> Y := X; -- Is this legal? > > (HALT is a run-time issue that has no impact here.) If you cannot decide if X is "initialized", then you cannot decode whether the program is legal. However you could define some set of pragmatic rules with either many false positives or many false negatives, or even mixed. These rules will be most likely observed as arbitrary by laymen. I don't think the issue deserves this. > While this snippet would not be legal as is (on purpose!), > Ada's case coverage rules can make the programmer write a > legal program easily: write an else branch! And this one: procedure Foo (X : in out Car); ... begin Foo (X); Y := X; -- Is this legal? Probably, already the call to Foo is illegal? And if Foo were declared as procedure Foo (X : out Car); >>> Does the phrase "first value" make sense? >> >> An object shall not have invalid values. All values are valid if the >> language is typed. Enforcing user-defined construction including >> prohibition of certain kinds of construction (e.g. per default constructor) >> is a different story. > > If you feed this to a Java compiler you will see how it is done. > The Java compiler will not accept a reference to a variable's > component when the variable may not have been initialized. I consider this model wrong. It is better not to introduce inappropriate values rather than trying to catch them later. Java does not have constrained types, so I can understand why they go this way. I think it is better to ensure that a declared value is initialized at the declaration point. I also think that forward uninitialized declarations represent bad style, e.g.: function Foo (...) return Bar is Result : Bar; begin ... if ... then raise Baz; end if; ... Result := ...; ... return Result; end Foo; I understand the motivation to declare Result uninitialized (because we could leave Foo via an exception), but I don't like this. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Georg Bauhaus on 1 Dec 2009 12:52
Dmitry A. Kazakov schrieb: > On Tue, 01 Dec 2009 16:02:21 +0100, Georg Bauhaus wrote: > >> Dmitry A. Kazakov schrieb: >>> On Tue, 01 Dec 2009 13:13:29 +0100, Georg Bauhaus wrote: >>> >>>> Then we could rely on the language: compilers will detect >>>> uninitialized variables provided these do not have a pragma/keyword/... >>>> to say that uninitialized is what the programmer wants. >>>> Some fancy means to tell the compiler that this variable >>>> does indeed have a good first value like pragma Import. >>>> >>>> X : [constant] Car; -- default init, >>> The error is here! >>>> -- undefined, >>>> -- junk bits. Doesn't matter >>>> -- *no* pragma Import (Ada, X); >>>> >>>> begin >>>> >>>> Spare := X.Tire (5); -- would become illegal, >>> Not here! >> Why? > > Because X is illegal right after begin: > > IF accessing X is illegal THEN the corresponding operation does not belong > to the type of X THEN the type of X is not Car. q.e.d. But the implications of this proof are purely formal, and not relevant before X is used. There is no way to perform an operation involving X in its own declaration. The difference in views would be that your laws say Don't create objects that could be used illegally if there were uses that can't be there, though, but for formal reasons. Whereas Java's ruling says (at compile time) Your program cannot be accepted because this object cannot be in a legal state here. The variable may not have been assigned a value. > (Provided, we are talking about a typed language) I think there is more in what you say than what is covered by the words "typed language"? >>> ------------------------- >>> Anyway, you cannot do that because: >>> >>> if HALT (P) then >>> X := Z; >>> end if; >>> Y := X; -- Is this legal? >> (HALT is a run-time issue that has no impact here.) > > If you cannot decide if X is "initialized", But I can decide whether (and when!) X is "initialized"! The compiler does not need to run HALT in order to see that X may not have been initialized when the condition is not true. The program is not accepted because it may lack an assignment to X before Y := X for much simpler reasons. In fact, SPARK marks it as error. I made a simple example, a procedure that does or does not assign depending on an unknown Boolean Condition parameter: 1 package body Asgn is 2 3 procedure Exmpl (Condition: Boolean; Result : out Integer) is 4 X : Integer; 5 begin 6 if Condition then 7 X := 42; 8 end if; 9 10 Result := X / 2; ^1 ??? ( 1) Flow Error :501: Expression contains reference(s) to variable X, which may have an undefined value. 11 end Exmpl; ??? ( 2) Flow Error :602: The undefined initial value of X may be used in the derivation of Result. 12 13 end Asgn; What the new rule would do is merge the two messages into one message about X that may not have a value yet: An "undefined initial value" MUST not be used like it is used on line 10. The (different) Ada language rule will forbid. >> While this snippet would not be legal as is (on purpose!), >> Ada's case coverage rules can make the programmer write a >> legal program easily: write an else branch! > > And this one: > > procedure Foo (X : in out Car); > ... > begin > Foo (X); > Y := X; -- Is this legal? Yes, this is legal, because Foo is called with X having been assigned a value. It cannot be otherwise, the recursion has to start somewhere. It can only start with an actual parameter that has a value (again, the compiler can check this). > And if Foo were declared as > > procedure Foo (X : out Car); We'd have roughly the same as this: X : Car; begin X := Foo_as_function; -- now X can be used I see no operational problem. Is there one? >>>> Does the phrase "first value" make sense? >>> An object shall not have invalid values. All values are valid if the >>> language is typed. Enforcing user-defined construction including >>> prohibition of certain kinds of construction (e.g. per default constructor) >>> is a different story. >> If you feed this to a Java compiler you will see how it is done. >> The Java compiler will not accept a reference to a variable's >> component when the variable may not have been initialized. > > I consider this model wrong. It is better not to introduce inappropriate > values rather than trying to catch them later. The Java rule works at compile time. No value is introduced at any time during compilation. Nothing to catch. A reference to a variable in source text is permitted if and only if the compiler can show, by following simple compile time rules, that a value has been assigned to the variable or constant prior to referencing. It need not evaluate calls (i.e. run the program) to arrive at a decision. > Java does not have > constrained types, so I can understand why they go this way. Ehm, I don't see the connection here. Which one is it? When I declare X : Some_Type(Some_Constraint); begin -- X may need further "initilization", and assigments, since -- Some_Type is an "open minded" type of a varying nature, -- not a fixed value. Its objects accumulate values. > I also think that forward uninitialized declarations represent bad > style, e.g.: > > function Foo (...) return Bar is > Result : Bar; > begin > ... > if ... then > raise Baz; > end if; > ... > Result := ...; > ... > return Result; > end Foo; > > I understand the motivation to declare Result uninitialized (because we > could leave Foo via an exception), but I don't like this. > But assigning the first value when declaring X won't help when the initialization can raise exceptions. How could this change? When the body of Foo gradually operates on Result to produce its final state (in a safe way because no reference can be made to Result or its parts without prior assignments), why should I pretend that any valid initial value for Result, provided by an initialization expression, is better than its default value? (Assuming that I cannot refer to "invalid" components of objects because the compiler will simply reject a program that might try.) |