Dynamic Validation of Programs Using Assertion Checking Facilities

[[abstract]]Automated dynamic validation through assertion checking has been proposed to ensure program correctness. This method has shown to be useful for validating large scale programs. When used in parallel with debugging aids, it can be useful for early detecting and properly locating errors. This paper provides a theoretical basis for assertion checking with regard to validation of program correctness. This gives some guidelines for inserting assertions within the program. An assertion language is provided for stating assertions. Salient features of this language are provided. A language preprocessor is designed to process source program inserted with assertions to generate source code acceptable to the existing compiler. Finally, future extensions to the assertion language and limitations of assertion checking to ensure program correctness are discussed[[fileno]]2030201030065[[department]]資訊工程學