Source code generating apparatus, source code proving apparatus, source code generating method, and source code generating program

摘要

The source code generated from the software specification written in formal language is the result of refining the above software and proves that it is the source code for realizing the above software. A scheduler editing means for editing a scheduler which defines at least a control structure including an if conditional branch structure and a do loop structure and a source code including at least an if conditional branch structure or a do loop structure from the software specification and the edited scheduler Scheduled model generation means for generating a Scheduled model including a control structure described in a formal language from a software specification and an edited scheduler, a software specification and an edited scheduler written in a programming language , If conditional branching structure and do loop structure are not included, a Flattened code generating means for generating a Flattened code including a goto sentence.