Abstract

A specification language is presented which provides three specification-building operators: amalgamated union, renaming and restriction. The language is enhanced with parameterization over higher-order variables based on the simply typed lambda calculus. Context dependencies that ensure the well-definedness of a parameterized specification, are defined over a calculus of requirements and can be syntactically derived. A contextual proof system for parameterized specifications is also presented, that is correct and relatively complete