An implicit-invocation language and its implementation

With the growing size and complexity of software systems, software verification and validation (V&V) is becoming more and more important. Formal verification and testing are two main methods for software verification and validation. Formal methods focus on the mathematical model of the program, and testing focuses on the actual program behavior. While testing can only be carried out with the actual programs, formal methods only work on models built with special modelling languages which are usually not executable. In this thesis, we designed a software V&V system that makes both formal verification and testing available to a program. The system includes a new programming language---Implicit-Invocation Language (II language), an II to XML transformation tool and an II to Turing Plus transformation tool. The II language is a programming language that encapsulates the concepts and semantics of implicit-invocation software systems. With the II to XML transformation tool, an II program can be translated into XML to be used as input to an existing model checking system for formal verification. With the II to Turing Plus transformation tool, an II program can be translated into Turing Plus for execution and testing.