Safe Compositional Specification of Networking Systems: A Compositional Analysis Approach
Kfoury, Assaf J.
Bradley, Adam D.
MetadataShow full item record
We present a type inference algorithm, in the style of compositional analysis, for the language TRAFFIC—a specification language for flow composition applications proposed in —and prove that this algorithm is correct: the typings it infers are principal typings, and the typings agree with syntax-directed type checking on closed flow specifications. This algorithm is capable of verifying partial flow specifications, which is a significant improvement over syntax-directed type checking algorithm presented in . We also show that this algorithm runs efficiently, i.e., in low-degree polynomial time.