Titlebook: KORSO: Methods, Languages, and Tools for the Construction of Correct Software; Final Report Manfred Broy,Stefan Jähnichen Book 1995 Springe

hemoglobin

Design of modular software systems with reuse,applications. The approach uses the representation of the development process of software as a graph and instantiates the notion of components as nodes and the notion of causal relations between these components as edges of the graph. A formal method for the systematic reuse of components is propose

Credence

AVL trees revisited: A case study in Spectrum,ich is organized in four stages: requirement specification, design specification, executable specification and functional program. The concept of AVL trees serves as example for presenting this approach.

隐士

laparoscopy

A fine-grain sort discipline and its application to formal program construction,s presented in more detail: A sort discipline is introduced to describe regular sets of ground constructor terms as extensional sorts. It is extended to cope with regular sets of ground substitutions, thereby allowing to compute different sorts for terms with different variable bindings. An algorith

代替

,TROLL light — The language and its development environment,r work focuses on the specification language TROLL . which allows to describe the part of the world to be modeled as a community of concurrently existing and communicating objects. Our specification language comes along with an integrated, open development environment. The task of this environment i

消耗

虚假

eucalyptus

Cytology

陈腐的人

,Seduct — A proof compiler for first order logic, obligations arising during the process of software verification. We will mainly describe those features of . which distinguish this theorem prover from other theorem provers and which make it especially suited for software verification.