[Issue 5007] @outer() attribute

[d-bugmail at puremagic.com]

https://d.puremagic.com/issues/show_bug.cgi?id=5007



--- Comment #5 from bearophile_hugs at 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: -------