Implement the decomposition theorem on CspCASL views

[csliam]

Implement the decomposition theorem on CspCASL refinements (represented as views). The theorem states

(D,P) ~~>_\sigma (D',P')

iff

D ~~>_\sigma D' and (D',\sigma(P)) ~~> (D', P')

where ~~> means refinement (i.e. a view) and sigma is a morphism.

A test specification for this could be:

library Buffer

logic CASL

spec List =
  sort Elem
  free type List ::= nil | cons(Elem; List)
  ops last: List -> ? Elem;
      rest: List -> ? List
end

spec List2 = List then
     op first : List ->? Elem
end

logic CspCASL

spec Buffer =
  data List
  channel read, write : Elem
  process Buf(List): read, write, List;
          EmptyBuffer : read,write, List;
          Buf(l)= read? x :: Elem -> Buf( cons(x,nil) ) []
                  (if l=nil then STOP else write!last(l) -> Buf( rest(l) ))
          EmptyBuffer = Buf(nil)
end

spec Buffer2 =
  data List2
  channel read, write : Elem
  process Buf(List): read, write, List;
          EmptyBuffer : read,write, List;
          Buf(l)= read? x :: Elem -> Buf( cons(x,nil) ) []
                  (if l=nil then STOP else write!last(l) -> Buf( rest(l) ))
          EmptyBuffer = Buf(nil)
end

view Hugo: Buffer to Buffer2

[maeder]

These are several tasks.

1. A theorem link (created by a view) between two nodes for a logic with a data logic (like CspCASL) and different incoming data nodes should not be localized. Till, is this the rule for local inference?

2. A new view for the (untranslated) data nodes should be created and a new node as new source for the Csp-link that relies on the target data node.