CATS Categorical model for Floyd-Hoare logic?

CATS Categorical model for Floyd-Hoare logic?

[David Espinosa]

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

Re: CATS Categorical model for Floyd-Hoare logic?

[Vaughan Pratt]

>Has there been work on a categorical model for "while programs" (or,
>equivalently, assembly language) and Floyd-Hoare logic?

The first such was developed by Arbib and Manes in the mid-70's.  Manes
went on to develop the theory in great detail, writing a near-book-length
article on it a decade later, not sure where it appeared.

  (1) What is the structure of this category?

As I recall it was an additive (semiadditive?) category, with sequential
composition represent by composition, and choice by sum within homsets.
The objects were predicates, the arrows were programs (aka predicate
transformers).

      Does it have products, sums, etc?  What program constructs do they
      correspond to?

Not sure about products, but it certainly had sums.  which was how
if-then-else was handled.

  (2) What is the correct equality on arrows?
 
My recollection is that it was fully abstract: the correct equality is
equality.

Vaughan Pratt