ISBN 0-948749-33-4, ©1995, Civil-Comp Limited, CIVIL-COMP Press 10 Saxe-Coburg Place, Edinburgh, EH3 5Br, UK


This paper illustrates the application of formal specification techniques to the experimental development of a software system for building-specification and automatic building-plan plotting.

Buildings are specified in an abstract way which records what the architect wants to build and not how it is actually built in terms of civil engineering materials. Building designs are not recorded in terms of their drawings but rather in a linguistic way, by structural composition of standard space units according to an abstract syntax equipped with space aggregation constructs, subject to invariant properties which check for building well-formedness.

A formal model is developed for such an abstract syntax and for its associated functionality which (as later prototyped in a rapid-prototyping shell) has mainly to do with automatically generating building plans from abstract descriptions. At prototype level, this is first achieved by structurally calculating LaTeX picture format drawings as a pictorial semantics of the abstract descriptions. In a second phase, the adopted output graphical server is the system.

Throughout these experiments, not only formal methods greatly increased confidence on the building-description language correctness, expressive power and conciseness, but also rapid prototyping provided a lot of insight on what one is designing, at a very low cost.

A prospect of implementation is given which not only will provide the system as a ``plug-in'' extension of for WINDOWS but also will connect it to an underlying production database allowing for automatic housing project materials planning and budget control.