I came to this forum via a chaotic search for methods to formally prove
program/algorithms correct. The vague hope is reinforced by what I
recently read in:
http://www-rocq.inria.fr/~dpotop/potopMemocodeBook.pdf
> The underlying synchronous model also allows the use of the well-studied
> functional verification techniques developed for synchronous circuits,..
I speculate/hope that the following is true and will bring me closer to
my destination;
- functional 'formatted' algorithms can be manipulated to prove
correctness;
- concatenative format can help the 'mathematical manipulations'
to prove correctness.
Is there any truth in this speculation/hope ?
And if so, can someone point me to text[s] which deals with the big
picture level of my goal.
I don't want to just analyse another way of saying "hello world".
Thanks,
== Chris Glur.