[Issue 5007] @outer() attribute

d-bugmail at puremagic.com d-bugmail at puremagic.com
Sun Mar 9 05:41:54 PDT 2014


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



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


More information about the Digitalmars-d-bugs mailing list