Next: Implementation Up: No Title Previous: Negation:

Verification of Formal Semantics

The verification of formal semantics specifications is an important issue since these specifications are usually designed by humans. We argue that sufficiently complex specifications most likely contain bugs or are even incomplete, if there exists no mechanical way to perform verification. DL systems always verify definitions (e.g. soundness of concepts, cyclic dependencies, contradictions, etc).

Another prominent feature of a DL system is a second reasoning component. Facts about individuals may be asserted as (unary or binary) predications (similar to Prolog style). These factual assertions are managed by an assertional reasoner whose function is to maintain current values for the types of all individuals in the assertional database. The type of an individual is the set of concepts that an individual in a database belongs to. We applied this reasoning to parsing of PJ programs.

In this sense, specifications expressed in DL become executable and can drive reasoning processes that implement visual parsing. The assertional reasoner can even support image interpretation by object classification (see [2]). We do not argue that this is the best or most efficient way to implement visual parsers. However, this free parser is only driven by our declarative specifications expressed in DL. The specifications can be readily verified by developing a set of well-designed example programs.

The verification process works as follows. Specifications of formal semantics and corresponding representations of example programs are analyzed by the DL system. Our taxonomy of concepts is designed in a way that every element of an example program has to be classified as an instance of a concept that marks legal interpretations. Elements that violate this property are an indication for a bug occurring in the example program or in the specifications.

Next: Implementation Up: No Title Previous: Negation: