Example informal specs
Module places_into_transition
Description
This module will examine the data
structures for the Petri net and create
a list of the places that have arcs
pointing into the transition.
Inputs
- param: transition #
- global: net
Outputs
- list of places (by reference)
- success indicator (by function return value)
Contract
- preconditions
- postconditions
- for class... class invariants
Assumptions
- module to be invoked via RPC from remote processes.
- transitions and places must be passed by generic numbers, not by internal
ids (such as pointers into structures) this module is to be an externally
invoked one
- Net (global) is unchanged by this module
Exceptions, special conditions or requirements
- must deal correctly with
- transition number does not exist
- transition number has no incident places
- output must distinguish between
- transition exists but has no incident places (empty list)
- transition does not exist so output list is empty
- performance issues
- system must return from call in no more than 5 ms.
Known Bugs (if any)
- this is not really a "requirement" section for specifying
the module behavior... rather, it is a warning for developers
if the module is in use, but still not quite right.