Convention for naming of packages

Le Fri, 17 Feb 2012 22:53:49 +0100, Manuel Collado
<m.collado@domain.invalid> a écrit:
> At first glance, it seems more "natural":
>
> X -> X
> X' -> X1
> X'' -> X2
> etc.

Good point indeed. While X2 may more clearly express this is a value of X
derived from X, I agree this seems odd to have X' = X2, X'' = X3 andso on.

Will balance yours and mine. Thanks for the comment Manuel, will keep it
in mind :-)

--
“Syntactic sugar causes cancer of the semi-colons.� [1]
“Structured Programming supports the law of the excluded muddle.� [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

On Feb 16, 9:44*am, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Le Thu, 09 Feb 2012 22:10:12 +0100, Yannick Duchêne (Hibou57)
> <yannick_duch...@yahoo.fr> a écrit:
>
> > Hi people out there,
>
> With functional representation in mind, when an object X' is a value
> derived from an object X in a recursive algorithm, which way do you name
> both X and X', as the Prime symbol is not allowed in Ada names?
>
> * * X1 and X2 ?
> * * X_1 and X_2 ?
> * * X and X2 ?
> * * X and X_2 ?
> * * X and X_Prime ?
> * * X and New_X ?
> * * X and Derived_X ?

It looks like Unicode characters 02B9 and 02CA are both allowed in
identifiers. Maybe you could one of those as your prime symbol?

-- Adam

Le Sat, 18 Feb 2012 00:52:41 +0100, Adam Beneschan <adam@irvine.com> a
écrit:
> It looks like Unicode characters 02B9 and 02CA are both allowed in
> identifiers. Maybe you could one of those as your prime symbol?

I've just checked, U+02CA is an accent, U+02B9 is a prime (as a modifier
letter, not a standalone glyph). At least GNAT reject it. Will check the
RM tomorrow (if ever GNAT is wrong).

Thanks for the point anyway, Adam.

--
“Syntactic sugar causes cancer of the semi-colons.� [1]
“Structured Programming supports the law of the excluded muddle.� [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Le Sat, 18 Feb 2012 01:24:40 +0100, Yannick Duchêne (Hibou57)
<yannick_duchene@yahoo.fr> a écrit:
> I've just checked, U+02CA is an accent, U+02B9 is a prime (as a modifier
> letter, not a standalone glyph). At least GNAT reject it. Will check the
> RM tomorrow (if ever GNAT is wrong).

No, GNAT is right, and I was wrong. Xʹ is OK and just requires to pass
“-gnatiw -gnatW8� options to GNAT.

“-gnatiw�: allows character code out of ASCII in names.
“-gnatW8�: tell GNAT the source file is UTF-8 encoded.

“-gnatW8� works alone, but I feel its safer to use “-gnatiw -gnatW8�, to
be more explicite.

Xʹ looks very similar to X' (attribute, type qualification), although the
compiler will probably help to catch it. This depends on font too.

XËŠ is far less similar to X', but does not really stands for prime,it
precisely is “Modifier Letter Acute Accent�. But don't bother, as the
effective meaning is clear.


--
“Syntactic sugar causes cancer of the semi-colons.� [1]
“Structured Programming supports the law of the excluded muddle.� [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

On 16.02.12 18:44, Yannick Duchêne (Hibou57) wrote:
> Le Thu, 09 Feb 2012 22:10:12 +0100, Yannick Duchêne (Hibou57) <yannick_duchene@yahoo.fr> a écrit:
>
>> Hi people out there,
>
> With functional representation in mind, when an object X' is a value derived from an object X in a recursive algorithm, which way do you name both X and X', as the Prime symbol is not allowed in Ada names?
>
> * X1 and X2 ?
> * X_1 and X_2 ?
> * X and X2 ?
> * X and X_2 ?
> * X and X_Prime ?
> * X and New_X ?
> * X and Derived_X ?

XX for x', XS for lists.

If both a letter with prime and a letter with plural s occur
in the same function, I'd choose a different prefix letter
for either.

Le Sat, 18 Feb 2012 12:32:40 +0100, Georg Bauhaus
<rm.dash-bauhaus@futureapps.de> a écrit:

> On 16.02.12 18:44, Yannick Duchêne (Hibou57) wrote:
>> Le Thu, 09 Feb 2012 22:10:12 +0100, Yannick Duchêne (Hibou57)
>> <yannick_duchene@yahoo.fr> a écrit:
>>
>>> Hi people out there,
>>
>> With functional representation in mind, when an object X' is a value
>> derived from an object X in a recursive algorithm, which way do you
>> name both X and X', as the Prime symbol is not allowed in Ada names?
>>
>> * X1 and X2 ?
>> * X_1 and X_2 ?
>> * X and X2 ?
>> * X and X_2 ?
>> * X and X_Prime ?
>> * X and New_X ?
>> * X and Derived_X ?
>
> XX for x', XS for lists.

XS seems Okay for lists, while it may conflict with package names if you
use plural for these too.

XX seems Okay for X', except when X is a longer name.

> If both a letter with prime and a letter with plural s occur
> in the same function, I'd choose a different prefix letter
> for either.

Right, but then, there is typically something like Head and Tail in the
place, which does not use the plural. So this does not may not necessarily
be an issue.


--
“Syntactic sugar causes cancer of the semi-colons.� [1]
“Structured Programming supports the law of the excluded muddle.� [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

On 02/17/2012 07:50 PM, Yannick Duchêne (Hibou57) wrote:
> Le Sat, 18 Feb 2012 01:24:40 +0100, Yannick Duchêne (Hibou57)
> <yannick_duchene@yahoo.fr> a écrit:
>> I've just checked, U+02CA is an accent, U+02B9 is a prime (as a
>> modifier letter, not a standalone glyph). At least GNAT reject it.
>> Will check the RM tomorrow (if ever GNAT is wrong).
>
> No, GNAT is right, and I was wrong. Xʹ is OK and just requires to pass
> “-gnatiw -gnatW8� options to GNAT.
>
> “-gnatiw�: allows character code out of ASCII in names.
> “-gnatW8�: tell GNAT the source file is UTF-8 encoded.
>
> “-gnatW8� works alone, but I feel its safer to use “-gnatiw -gnatW8�, to
> be more explicite.
>
> Xʹ looks very similar to X' (attribute, type qualification), although
> the compiler will probably help to catch it. This depends on font too.
>
> XËŠ is far less similar to X', but does not really stands for prime, it
> precisely is “Modifier Letter Acute Accent�. But don't bother, as the
> effective meaning is clear.
>
>
Just don't use a name like XʹFirst :-) What about Xʹs for plural?

--
---
BrianG
000
@[Google's email domain]
..com

BrianG <me@null.email> writes:

> What about Xʹs for plural?

No, no!

http://en.wikipedia.org/wiki/Apostro...strophes.22.29

On Feb 16, 5:44Â*pm, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> With functional representation in mind, when an object X' is a value
> derived from an object X in a recursive algorithm, which way do you name
> both X and X', as the Prime symbol is not allowed in Ada names?

To refer to before and after values of a variable in e.g. a
postcondition, the convention of suffixing a subscript-zero to denote
the before value is fairly common in formal methods texts, e.g. the
classic "Programming from Specifications":
http://www.cs.ox.ac.uk/publications/books/PfS/
So, for example, the postcondition
X = Xâ‚€ + 1
says that the value of X is increased by 1. Perhaps an ASCII
equivalent would be
X = X_0 + 1

I've come across exactly this conflict with primes in the past. The
Ada verification tool, DAZ - built on ProofPower, see
http://www.lemma-one.com/ProofPower/index/
- would have ideally used a prime to denote an after value because
that is the convention of the Z notation, the language used to express
pre- and postconditions of Ada statements. Instead it uses a
subscript-zero for the before value, like in Programming from
Specifications, on which it was based.

Phil

Le Sun, 19 Feb 2012 19:07:15 +0100, Phil Clayton
<phil.clayton@lineone.net> a écrit:
> To refer to before and after values of a variable in e.g. a
> postcondition, the convention of suffixing a subscript-zero to denote
> the before value is fairly common in formal methods texts, e.g. the
> classic "Programming from Specifications":
> http://www.cs.ox.ac.uk/publications/books/PfS/
> So, for example, the postcondition
> X = Xâ‚€ + 1
> says that the value of X is increased by 1. Perhaps an ASCII
> equivalent would be
> X = X_0 + 1

Prior side note: I’ve checked GNAT reject it, the ₀, with a message
“invalid wide character in identifier�, and this time, that's not due to
missing compiler options. Will really need to check the RM for these
characters, so my comments may not not relevant.

Xâ‚€ or X_0 Could be an option if everything was formal in a given
application. But when a specification is expected to be exposed with a
classic look, this would imply giving subprograms argument names like Xâ‚€
or X_0, as the “value before� is often from the subprogram parameters, and
this wouldn't look as expected.

May be OK or not, depending on the overall style of an application.

But you gave me the idea X�, X₂, X₃ could be alternatives to Xʹ or Xˊ,
more distinctive, except it may make readers think they are list indexes
or polynomial indexes…

Hint: ₀ is U+2080, � is U+2081, and so on, up to ₉.. Use of a character
palette is probably recommended to help.


> http://www.cs.ox.ac.uk/publications/books/PfS/
> […]
> I've come across exactly this conflict with primes in the past. The
> Ada verification tool, DAZ - built on ProofPower, see
> http://www.lemma-one.com/ProofPower/index/

Cool links, especially the former :-) Thanks

--
“Syntactic sugar causes cancer of the semi-colons.� [1]
“Structured Programming supports the law of the excluded muddle.� [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

On Feb 19, 9:53Â*pm, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Le Sun, 19 Feb 2012 19:07:15 +0100, Phil Clayton
> <phil.clay...@lineone.net> a écrit:
>
> > To refer to before and after values of a variable in e.g. a
> > postcondition, the convention of suffixing a subscript-zero to denote
> > the before value is fairly common in formal methods texts, e.g. the
> > classic "Programming from Specifications":
> >http://www.cs.ox.ac.uk/publications/books/PfS/
> > So, for example, the postcondition
> > Â* X = Xâ‚€ + 1
> > says that the value of X is increased by 1. Â*Perhaps an ASCII
> > equivalent would be
> > Â* X = X_0 + 1
>
> Prior side note: I’ve checked GNAT reject it, the ₀, witha message
> “invalid wide character in identifier�, and this time, that's not due to
> missing compiler options. Will really need to check the RM for these
> characters, so my comments may not not relevant.
>
> Xâ‚€ or X_0 Could be an option if everything was formal in a given
> application. But when a specification is expected to be exposed with a
> classic look, this would imply giving subprograms argument names like Xâ‚€
> or X_0, as the “value before� is often from the subprogram parameters, and
> this wouldn't look as expected.
>
> May be OK or not, depending on the overall style of an application.
>
> But you gave me the idea X�, X₂, X₃ could be alternatives to Xʹ or Xˊ,
> more distinctive, except it may make readers think they are list indexes
> or polynomial indexes…
>
> Hint: ₀ is U+2080, � is U+2081, and so on, up to ₉. Use of a character
> palette is probably recommended to help.

For before and after values, perhaps X_Old and X is worth considering
- then a postcondition e.g.
X = X_Old + 1
would look more like it would for a program with a destructive update
of X:
X = X'Old + 1


> >http://www.cs.ox.ac.uk/publications/books/PfS/
> > […]
> > I've come across exactly this conflict with primes in the past. Â*The
> > Ada verification tool, DAZ - built on ProofPower, see
> >http://www.lemma-one.com/ProofPower/index/
>
> Cool links, especially the former :-) Thanks

I don't know of anyone who actually derives programs for real as
described in PfS, but understanding the formal program development
methods helps one justify or explain a program - not necessarily a
formal argument but perhaps just better comments or more useful pre/
postconditions for run-time checking.

The DAZ tool checks PfS-style refinement arguments. For example

� X [ true, X = X₀ + 1 ]
⊑
X := X + 1;

would produce a verification condition, which, if provable means that
the code is a valid implementation of the specification statement. As
far as I know, DAZ was never used to develop programs (as described in
PfS) but to check already written programs against a specification by
'recovering' a refinement that gave provable verification conditions.
Then, verification conditions are shown to be provable by proving them
- the subject of theorem proving is yet another (fascinating) world.
Use of such tools tends to be limited to very critical systems. In
fact, the analysis is very similar to compliance analysis with the
SPARK examiner, though the presentation is very different.

Phil

"Simon Wright" <simon@pushface.org> wrote in message
news:m2r4xr13b2.fsf@pushface.org...
> BrianG <me@null.email> writes:
>
>> What about X's for plural?
>
> No, no!
>
> http://en.wikipedia.org/wiki/Apostro...strophes.22.29

Cool. I always thought that the 's plurals littering the comments in
Janus/Ada (put there by others; I'm forever removing them) were illiteracy,
but now I know that they are just archaic. Big difference. :-)

Randy.