Synchrnous languages have been designed to ease the developement of reactive system, by providing a methodological framework for assisting system designers from the early stages of requirement specifications to the final stages of code generation or circuit production. Synchronous languages enable a very high-level specification and an extremely modular design of complex reactive systems. We define an order-theoretical model that gives a unified mathematical formalization of all the above aspects of the synchronous methodology (from relations to circuits). The model has been specified and vaidated using a theorem prover as part of the certified, reference compiler of a synchronous programming language.
展开▼
