5 Pretty printer	Top	7 Showing module dependencies
6 Confidence condition generation

6 Confidence condition generation

The confidence condition generator was written by Tan Xinming.

Confidence conditions are conditions that should generally be true if the module is not to be inconsistent, but that cannot in general be determined as true by a tool. The following conditions are generated (provided the type checker first runs successfully):

1. Arguments of invocations of functions and operators are in subtypes, and, for partial functions and operators, preconditions are satisfied.

2. Values supposed to be in subtypes are in the subtypes. These are generated for

   • values in explicit value definitions;

   • values of explicit function definitions (for parameters in appropriate subtypes and satisfying any given preconditions);

   • initial values of variables;

   • values assigned to variables;

   • values output on channels.

3. Subtypes are not empty.

4. Values satisfying the restrictions exist for implicit value and function definitions.

5. The classes of actual scheme parameters implement the classes of the formal parameters.

6. For an implementation relation or an implementation expression, the implementing class implements the implemented class. This gives a means of expanding such a relation or expression, by asserting the relation in a theory and then generating the confidence conditions for the theory.

7. A definition of a partial function without a precondition (which generates the confidence condition false).

8. A definition of a total function with a precondition (which generates the confidence condition false).

Confidence conditions are output on standard output. They take the form

X.rsl:m:n CC:
- comment on source of condition
condition

Examples of all the first 4 kinds of confidence conditions listed above are generated from the following intentionally peculiar scheme (in which line numbers have been inserted so that readers can relate the following confidence conditions to their source):

 1 scheme CC = 
 2 class
 3   value
 4     x1 : Int = hd <..>,
 5     x2 : Int = f1(-1),
 6     x3 : Nat = -1,
 7     f1 : Nat -~-> Nat
 8     f1(x) is -x
 9     pre x > 0
10   variable
11     v : Nat := -1
12   channel
13     c : Nat
14   value
15     g : Unit -> write v out c Unit
16     g() is v := -1 ; c!-1
17   type
18     None = {| i : Nat :- i < 0 |}
19   value
20     x4 : Nat :- x4 < 0,
21     f2 : Nat -> Nat
22     f2(n) as r post n + r = 0
23 end

This produces the following confidence conditions (which are all provably false):

Checking CC ... 
Finished CC
CC.rsl:4:19: CC:
-- application arguments and/or precondition
let x = <..> in x ~= <..> end

CC.rsl:5:18: CC:
-- application arguments and/or precondition
-1 >= 0 /\ let x = -1 in x > 0 end

CC.rsl:6:14: CC:
-- value in subtype
-1 >= 0

CC.rsl:8:5: CC:
-- function result in subtype
all x : Nat :- (x > 0 is true) => -x >= 0

CC.rsl:11:13: CC:
-- initial value in subtype
-1 >= 0

CC.rsl:16:17: CC:
-- assigned value in subtype
-1 >= 0

CC.rsl:16:24: CC:
-- output value in subtype
-1 >= 0

CC.rsl:18:26: CC:
-- subtype not empty
exists i : Nat :- i < 0

CC.rsl:20:8: CC:
-- possible value in subtype
exists x4 : Nat :- x4 < 0

CC.rsl:22:5: CC:
-- possible function result in subtype
all n : Nat :- exists r : Nat :- n + r = 0

rsltc completed: 10 confidence condition(s) generated
rsltc completed: 0 error(s) 0 warning(s)

In the case of implementation relations and conditions, the confidence condition is typically the conjunction of a number of conditions, each of which also has a file:line:column reference, followed by IC: (to indicate an implementation condition), plus some text, as a comment in the condition. Usually these references are to the appropriate place in the implementing class, but in the case of an axiom in the implemented class they are to the axiom, since this will typically have no equivalent in the implementing class.

In general, confidence conditions are not generated for definitions that are syntactically identical in the implementing and implemented classes.

For example, consider the schemes A0 and A1 and the theory A_TH below that asserts that A1 implements A0:

Generating confidence conditions for A_TH produces the following output:

Loading A0 ... 
Loaded A0
Loading A1 ... 
Loaded A1
Checking A_TH ... 
Finished A_TH
A_TH.rsl:4:12: CC:
-- implementation conditions:
in A1 |- 
  -- A1.rsl:5:7: IC: value definition changed
  y > 1 /\ 
  -- A0.rsl:10:9: IC: [x_pos]
  x > 0

rsltc completed: 1 confidence condition(s) generated
rsltc completed: 0 error(s) 0 warning(s)

This confidence condition can be proved.

6 Confidence condition generation
5 Pretty printer	Top	7 Showing module dependencies