Closed omltcat closed 6 months ago
@omltcat I haven't looked at all of the details of the spec from @CynthiaLiu0805, but what I see above can work. The main method is changing the state of other modules, which means this is a state transition. The way the specification is given is operational, rather than descriptive. An operational spec is an algorithm, while a descriptive spec is a mathematical spec of what what happens, without saying how it happens. We like descriptive specifications, since they are more abstract, but in some cases the operational spec makes the most sense. A case like this seems appropriate for an operational spec. I used a similar specification in the SWHS example.
I think transition here specifically means the changes to the state variables, not the workflow of this module. I ran into this problem as well. I want to explain how the module works, apart from transition/output/exception, but don't know where to put it. Maybe Dr. Smith can explain this more? @smiths