Description style of model-based formal specification considering executability and readability

In this paper, we propose description style of model-based formal specification considering an executability for verification and a readability. We use model-based formal specification language VDM++. In a software development, a role of specification and that of design are often distinguished. If this boundary is ambiguous, designers can not understand a scope of specification and design. In an executable specification, there are mechanisms of execution and description of specifications. If this boundary is ambiguous, it is hard to understand a specification. First, we focus on the internal data structure as a boundary between specification and design. We propose techniques of hiding types that are outside the scope of specification. We compare the differences in a readability by use of hiding techniques. Next, in a executable specification, we examine a readability and an executability from the description style provided by the language specification of VDM++. Finally, we present the part of experimental results of ongoing project.