Home » forums » LtU Forum

wither formal methods?

I sometimes get a bee in my bonnet to look for tools to do model driven design and the like. So, I found a list of verification and synthesis tools. The mind boggles. For little people such as myself, I wish there were a table somewhere that listed the range of features and then showed what each system did/not support. I want stuff that would help with application development: user interface and state machine (e.g. audio playback engine + ui controlling it) type modeling and code generation (and round tripping). Anybody know of such guidance for the laymen?

By raould at 2014-07-22 00:09 | LtU Forum | previous forum topic | next forum topic | other blogs | 3146 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

whence formal methods?

(for anyone interested in the flip side: Floyd "Assigning Meanings to Programs", 1967 is commonly considered seminal, but even there he notes

... we may prove certain properties of programs, particularly properties of the form: "If the initial values of the program variables satisfy the relation R1, the final values on completion will satisfy the relation R2." Proofs of termination are dealt with by showing that each step of a program decreases some entity which cannot decrease indefinitely.
These modes of proof of correctness and termination are not original ...
Thanks to Maarten van Emden, I've learned that Goldstine and von Neumann were already using such modes in Planning and coding of problems for an electronic computing instrument (part II, 1947) ... does anyone know if similar verification modes were in use earlier —perhaps ca. 1930's in Eckert's circles?— for pre-computer automated processing?)

By Dave at Tue, 2014-07-22 10:22 | login or register to post comments