Re: Convention for naming of anything

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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