Guardol is a domain-specific language designed to facili tate the construction of correct network guards operating over tree shaped data. The Guardol system generates Ada code from Guardol programs and also provides specification and automated verification sup port. Guard programs and specifications are translated to higher order logic, then deductively transformed to a form suitable for a SMT-style decision procedure for recursive functions over tree-structured data. The result is that difficult properties of Guardol programs can be proved fully automatically.
展开▼
