Module dev.civl.sarl
Package dev.civl.sarl.IF

Interface ValidityResult

All Known Subinterfaces:
ModelResult
public interface ValidityResult

A ValidityResult represents the result of a validity query.

It defines an enumerated type ValidityResult.ResultType with three possible values: ValidityResult.ResultType.YES, ValidityResult.ResultType.NO, ValidityResult.ResultType.MAYBE. This is used to represent the result returned by an automated theorem prover.

In the case that the result type is ValidityResult.ResultType.NO, a ValidityResult may also provide a model, i.e., an assignment of concrete values to symbolic constants that leads the assumption to evaluate to true and the predicate to evaluate to false.

The subclass ModelResult provides a method to get a model (counterexample). A ModelResult always has result type ValidityResult.ResultType.NO, because only invalid queries can have models. However, the model returned may be null: this indicates that the attempt to find a model failed for some reason.

An instance of ValidityResult of type ValidityResult.ResultType.NO that is not an instance of ModelResult indicates that there was no attempt to find a model.

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Interface
    Description
    static enum 
    ValidityResult.ResultType
    The 3 kinds of results to the "valid" question: yes, no, or maybe (a.k.a, "I don't know").

  • Method Summary

    Modifier and Type
    Method
    Description
    ValidityResult.ResultType
    getResultType()
    Returns the result type of this result.

  • Method Details