Browse Source

Fix typos

CaseStudiesProcessDefinition
JoseRuizAdaCore 8 years ago committed by GitHub
parent
commit
2db3a72f11
  1. 2
      UseCaseDevelopment/Layer2_MMS_SW_SPARK/DESIGN.txt

2
UseCaseDevelopment/Layer2_MMS_SW_SPARK/DESIGN.txt

@ -28,7 +28,7 @@ ACTIVITIES:
+ Result: No inconsistency found. + Result: No inconsistency found.
2 - Review of the specification for translatability in Ada contracts: 2 - Review of the specification for translatability in Ada contracts:
Ruiz1306
* Design: * Design:
Each component provides a Run procedure located in a child package Comp.Behavior. This procedure is responsible from updating the internal state of the component at each step. Scheduling, as well as handling of inputs and outputs are not considered here. The procedure Run may have a contract, representing the part of its behavioural specification which is translatable into Ada contracts. Contracts from the specification document are stored in a distinct unit, named Comp.Behavior.Guarantees. Parts of specification contracts and of functional behaviours which are not fit for translation into SPARK contracts will be listed here. Each component provides a Run procedure located in a child package Comp.Behavior. This procedure is responsible from updating the internal state of the component at each step. Scheduling, as well as handling of inputs and outputs are not considered here. The procedure Run may have a contract, representing the part of its behavioural specification which is translatable into Ada contracts. Contracts from the specification document are stored in a distinct unit, named Comp.Behavior.Guarantees. Parts of specification contracts and of functional behaviours which are not fit for translation into SPARK contracts will be listed here.

Loading…
Cancel
Save