Lambda the Ultimate

Applies formal methods to visual programming mandated by industry standard. An embedded control system and programmable logic controller industry standard (IEC 1131-3) defines four DSL's that can be represented either diagrammatically or textually utilizing "circuit (i.e. box-and-wire) diagrams, emphasising a data-flow view" and "Petri net diagrams, suited to a control-flow view." (140) The author notes that in general "diagrams are a very natural syntax for software in certain domains; particularly those in which diagrammatic notations form an integral part of design practice and technical discourse" (139) and that "domain-specific representations of computer software should accord with, and ideally be derived from existing notations in the domain." (9) But deriving rigorous conclusions from common diagrammatic manipulation is not trivial:

"While the use of formal methods in supplying evidence is often recommended or mandated....their practical application remains undeniably difficult... ...many informal or semi-formal arguments are guided by the structure of some high-level representation of the system, such as a diagram...the elevation of such arguments to a level admissible as rigorous evidence requires their formal underpinning, validation and justification by logical means... our aim is to apply the theory connecting diagrammatic representations to semantics in seeking criteria under which representation-driven arguments are deemed sufficient to provide rigorous evidence without the need of explicitly constructing fully formal proofs. (144)"

Posted to DSL by jon fernquest on 8/2/02; 11:48:30 PM