کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
433782 | 1441675 | 2014 | 20 صفحه PDF | دانلود رایگان |
Flow networks are inductively defined, assembled from small components to produce arbitrarily large ones, with interchangeable functionally-equivalent parts. We carry out this induction formally using a domain-specific language (DSL). Associated with our DSL are a semantics and a typing theory. The latter gives rise to a system of formal annotations that enforce desirable properties of flow networks as invariants across their interfaces. A prerequisite for a typing theory is a formal semantics, i.e., a rigorous characterization of flows that are safe for the network (limited to the notion of feasible flows in this paper, unfeasible flows being considered unsafe). We give a detailed presentation of a denotational semantics only, but also point out the elements that an equivalent operational semantics must include.
► We define the formal syntax and semantics of a DSL for assembling flow-networks.
► The DSL supports an incremental-modular design and analysis of flow-networks.
► A denotational semantics of the DSL is given in detail.
► A typing system based on the denotational semantics is rigorously set up.
Journal: Science of Computer Programming - Volume 93, Part A, 1 November 2014, Pages 19–38