Here's an idea. Branching temporal logic (CTL) allow us to write a specification with modal operators like
"forever P", "eventually P" and "never P" and also consider different worlds by the usual quantifiers, ie:
"For all paths, P holds"
"There exists a path that P holds"
I think ctrees would work as a denotational model of CTL. Then we can have a CTL specification denote to a ctree S and show a program also denotes to a ctree P then prove P <= S where <= is the refinement operator.
elefthei
commented
1 year ago
Here's an idea. Branching temporal logic (CTL) allow us to write a specification with modal operators like "forever P", "eventually P" and "never P" and also consider different worlds by the usual quantifiers, ie: "For all paths, P holds" "There exists a path that P holds"
I think ctrees would work as a denotational model of CTL. Then we can have a CTL specification denote to a ctree
Sand show a program also denotes to a ctreePthen proveP <= Swhere<=is the refinement operator.