https://d.puremagic.com/issues/show_bug.cgi?id=5007
--- Comment #5 from bearophile_h...@eml.cc 2014-02-19 15:07:18 PST --- It seems this idea of mine isn't so crazy. This is from the SPARK 2014 sublanguage: http://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/14/140201-fosdem/03-ada-spark.pdf Clarify access to global variables: with Global => null; -- Not reference to global items with Global => V; -- V is an input of the subprogram with Global => (X, Y, Z); -- X, Y and Z are inputs of the subprogram with Global => (Input => V); -- V is an input of the subprogram. with Global => (Input => (X, Y, Z)); -- X, Y and Z are inputs of the subprogram with Global => (Output => (A, B, C)); -- A, B and C are outputs of the subprogram with Global => (In_Out => (D, E, F)); -- D, E and F are both inputs and outputs of -- the subprogram with Global => (Proof_In => (G, H)); -- G and H are only used in assertion -- expressions within the subprogram with Global => (Input => (X, Y, Z), Output => (A, B, C), In_Out => (P, Q, R), Proof_In => (T, U)); -- A global aspect with all types of global specification Clarify information flow: procedure P (X, Y, Z : in Integer; A, B, C : in out Integer; D, E out Integer) with Depends => ((A, B) =>+ (A, X, Y), C =>+ null, D => Z, E => null); -- The "+" sign attached to the arrow indicates self-dependency -- The exit value of A depends on the entry value of A as well as the entry -- values of X and Y. -- Similarly, the exit value of B depends on the entry value of B as well as -- the entry values of A, X and Y. -- The exit value of C depends only on the entry value of C. -- The exit value of D depends on the entry value of Z. -- The exit value of E does not depend on any input value. Comments: - Spark is even more strict, but this is expected, because it has to prove the code formally. - Probably for most usages an @outer() as explained, where listed outer scoped variables are "in" (not mutable) on default is enough, and it's easy to remember and use. - In the years I have had many bugs in the code caused by unwanted interactions with global variables. - The usage of @outer() is optional. There are many kinds of D code: small script-like programs, GUIs, videogames, heavy numeric software, large network applications, and so on. Some of such kinds of code don't need much contracts and they don't need @outer. But in larger programs, or programs where you want a partial integrity (where you can also use Ada), it's useful. -- Configure issuemail: https://d.puremagic.com/issues/userprefs.cgi?tab=email ------- You are receiving this mail because: -------