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



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

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



--- Comment #6 from bearophile_hugs@eml.cc 2014-03-09 05:41:50 PDT ---
The purpose of the "with Global" and "with Depends" annotations of SPARK2014 is to help mathematically prove that a function is correct. While the lighter and optional @outer() annotation I have suggested for D is useful to write unit tests and reason informally about code. If you have a function that reads and/or writes data from global (or outer) scope, it's not easy to set the global state to have reproducible unit tests. Writing unit tests could be hard. If such D functions are annotated with @outer() then writing unit tests becomes faster, safer and simpler.


Example: if you need to translate some BCPL code like this to D, full of global (untyped) variables, and you want (need) to add unit tests to make sure the translation is correct, you learn very quickly to appreciate an annotation like @outer(), that enforces what each function accesses from the global scope (later, when the D code works, you can refactor the code, moving most of those global variables in structs, putting them inside functions, passing them as arguments, etc. But it's not wise to make such changes as first step, because this could easily break the code):


GLOBAL {
xupb     : 200
yupb     : 201
spacev   : 202
spacet   : 203
spacep   : 204
boardv   : 205
knownv   : 206
xdatav   : 207
ydatav   : 208
xfreedomv: 209
yfreedomv: 210
change   : 211
tracing  : 212
rowbits  : 213
known    : 214
orsets   : 215
andsets  : 216
count    : 217
debug    : 218
}

AND blobs(v, upb) = VALOF
{ LET res = 0
  FOR i = 0 TO upb DO
  { LET p = v!i
    UNTIL !p=0 DO { res := res+!p; p := p+1 }
  }
  RESULTIS res
}

AND freedom(p, upb) = VALOF
{ IF !p=0 RESULTIS 0
  upb := upb - !p
  { p := p+1
    IF !p=0 RESULTIS upb+1
    upb := upb - !p - 1
  } REPEAT
}

AND allsolutions() BE
{ UNLESS solve() RETURN // no solutions can be found from here

  { LET b = VEC 31
    LET k = VEC 31
    LET pos, bit = 0, 0

    // save current state
    FOR i = 0 TO 31 DO b!i, k!i := boardv!i, knownv!i
    FOR i = 0 TO yupb DO
    { LET bits = NOT knownv!i
      UNLESS bits=0 DO
      { pos, bit := i, bits & -bits
        BREAK
      }
    }



If you read D code written by another person that uses few global variables, you will be glad if the code is annotated with @outer() because it makes it easier and faster to understand and modify the code.

-- 
Configure issuemail: https://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------