[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: What should I do next in the Hyperbook?




8. Something about writing informal specs.

 
 
I'm curious to know what you would put in such a section.
 
I definitely find it difficult to write correct informal spec of a true routine. Either it is
imprecise as in this page:
 
https://developer.gnome.org/glib/2.26/glib-String-Utility-Functions.html
 
or it is  rather difficult to know how to use it in practice. For instance as in:
 
http://frama-c.com/download/acsl-implementation-Sodium-20150201.pdf
 
But it is maybe due to the conciseness of the documentation. (And these ones are rather formal.)
 
Definitely I think that the use of what they now call "ghost variables" or "model variables"
is mandatory.
 
And there is still a lack of accurate and powerful tools. Notably to write easily true formal,
mathematical computer scince object in a language like TeX
(they have the property of being longer to write than the mathematical ones and it is a pain
to write them of change them).
 
But maybe you want to speak of the algorithm itself and the involved data structures.
Not its implementation.
 
--
FL