登入選單
返回Google圖書搜尋
註釋This facility is based on using two kinds of module: objects to encapsulate executable code, and in particular to define abstract data types by initial algebra semantics; and theories to specify both syntactic structure and semantic properties for modules and module interfaces. Each kind of module can be parameterized, where actual parameters are modules. For parameter instantiation, a view binds the formal entities in an interface theory to actual entities in a module, and also asserts that the target module satisfies the semantic requirements of the interface theory. Module expressions allow complex combinations of already defined modules, including sums, instantiations, and transformations; moreover, evaluating a module expression actually constructs the described software (sub)system from the given components.