The electronic articles are done!

Well, I got through the remaining 14 articles sitting in the thesis folder on my hard drive. This batch was considerably easier and more homogenous than yesterday's. Today I had:

  1. An article by Naumann on total-correctness semantics for an Oberon-like language (called Io - Idealized Oberon) with record-type, procedure-type, and global variables. The semantics uses a set-theoretic predicate transformer model, which sounds pretty interesting.
  2. A Cavalcanti and Naumann article on the semantics of ROOL involving specification statements in the language, or something like that. It appears that ROOL also uses a set-based predicate transformer semantics.
  3. And then I had 12 documents on SPARK from the good people at Praxis Critical Systems.

The SPARK articles included a number of case studies and a few articles on proving the absence of runtime exceptions. The MULTOS CA (a smart-card system) and SHOLIS (helicopter control system) were cited in several articles. SHOLIS is interesting because there was, apparently, a great deal of proof work done, both in SPARK and in Z. The MULTOS CA was interesting to me because of the use of off-the-shelf software in the form of Windows and MFC.

I think I can justify a light day on a Saturday, so that's about it. I do have some text files of notes that I need to link to the corresponding articles, so I'll probably do that tonight. I might start organizing my mind map as well, but I'll probably do the bulk of that tomorrow.

You can reply to this entry by leaving a comment below. This entry accepts Pingbacks from other blogs.

Add your comments #

A comment body is required. No HTML code allowed. URLs starting with http:// or ftp:// will be automatically converted to hyperlinks.