Re: Convention for naming of anything

[Phil Clayton <phil.clayton@lineone.net>]

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