FM Thesis

I've gotten through the remainder of my paper articles. I still have to go over my accumulated notes, but most of them are on the articles I've been cataloging here.

I had 10 articles today. They include:

1. An article describing a wp() refinement calculus. It seems to focus on a "refinement relation" for preserving total correctness between steps in program derivation.
2. An article on integrating FM into development. It describes the Secure Release Terminal (a system for changing classified document security) and the use of the the Ina Jo specification language.
3. An interesting article on teaching FM in a "general education" computer science course.
4. A paper describing KIDS, an interactive system for automatically developing programs. The idea is that all the hard work is automated and you can build a formal specification just by selecting various high-level transformations. It gives a derivation of a program to solve the k-queens problem as an example.
5. An interesting looking article on reasoning about the effects of program changes. It uses an approximate logic and works on the structure, rather than semantics, of the program.
6. Greg Nelson's generalization of Dijkstra's calculus. Essentially, he removed the Law of the Excluded Miracle, i.e. wp(S, false)=false. This gives us the possibility for partial commands and other things I don't want to think about at 10:30 at night.
7. A round-table series of articles on formal methods. It's just a series of one-page articles on FM topics ranging from education to industrial use.
8. An article on the Penelope "verification editor" for Larch/Ada. Apparently it's another interactive tool, but this one uses the Larch Shared Language to generate verification conditions for a subset of Ada.
9. A paper on "debugging" Larch specifications. It describes a couple of tools that check various claims that can be included in Larch specifications.
10. An article on using the Boyer-Moore prover to automatically verify concurrent programs. Describes the logic and semantics used and gives the example of a distributed program to compute a minimum value in a tree.

I guess tomorrow I'll pick up on finishing off my mind-map and start thinking about a topic summary. That should be interesting, as staying on topic was where I had my problems the first time.