How to represent sequential operation schemas [Z-notation]

Question

I have an operation schema C which consists of two sequential operation schemas A and B. A must be performed before B. I'm stuck on how to represent the sequence of schema activation.

Can I use schema conjunction, i.e. C == A ∧ B ? or is there a way to 'call' schema B from A?

I'm new to Z-notation, any help would be greatly appreciated!

Answer 1

For an example of a big Z specification, I suggest this recently uploaded project: https://github.com/vinahradau/finma

The following schema conjunction works in CZT. Here, C is not called from B, but rather after B.

─
  A == B ∧ C 
└

Answer 2

A schema is just a way of wrapping up a chunk of mathematics.

There is a fairly standard way of interpreting that mathematics as describing an ADT. One schema represents the state variables and constraints among them, one schema represents the initialisation, and as many schemas representing operations as there are operations in the ADT's interface.

You are probably looking for forward schema composition, C == A ⨟ B.