A tool for visual and formal modelling of software designs

• The paper presents the Visual Contract Builder (VCB) tool supporting the Visual Contract Language (VCL).
• VCL is a graphical language for describing software designs formally.
• VCL and VCB have been applied to several case studies.
• The paper evaluates VCB based on a survey carried out in the context of a controlled experiment.
• The paper includes several reflections on strengths and weaknesses of VCB and lessons learnt.

Diagrams are ubiquitous in software engineering and widely used for software modelling. The visual contract language (VCL) enables an approach to software design modelling that is entirely graphical and has a mathematical basis. VCL's main novelties lie in its capacity to describe predicates visually and in its graphical front-end to formal modelling. VCL is brought to life in the visual contract builder (VCB) tool presented in this paper. VCB provides diagram editors for the whole VCL suite, it type-checks diagrams and generates Z formal specifications from them; the Z specification enables formal verification and validation using Z theorem provers. The paper evaluates VCB based on the results of a survey carried out in the context of a controlled experiment. The work presented here is a contribution to the area of visual design modelling: the paper presents a state of the art tool supporting the novel VCL language and concrete empirical results on the usefulness and effectiveness of tool and language in particular, suggesting benefits of visual modelling in general.