14 Feb
1998
14 Feb
'98
1:40 a.m.
Hopefully this is my last question for a while. Has there been work on a categorical model for "while programs" (or, equivalently, assembly language) and Floyd-Hoare logic? In the obvious model, objects are predicates on a store, and arrows are code sequences mapping stores to stores that satisfy the postcondition assuming the precondition. I'm interested to know: (1) What is the structure of this category? Does it have products, sums, etc? What program constructs do they correspond to? (2) What is the correct equality on arrows? I would think that we want the finest equality that yields nice structure. Then we can collapse afterward to obtain coarser categories. David