160
% does provide thorough checking for small examples. (Given the
combinatorics, large
% examples are out of the question.
well_defined_for(LIST) :-
not(ordering_counterexample(LIST, A1, A2)),
not(nil_minimal_counterexample(LIST, A)).
% If there is an element not greater than nil, this predicate
determines its identity.
nil_minimal_counterexample(LIST, A) :-
legal_address_for(LIST, A),
A \= address([], 0),
not(less(address([], 0), A)).
% If there is a pair of addresses that is not properly ordered, this
predicate finds
% them.
ordering_counterexample(LIST, A1, A2) :-
legal_address_for(LIST, A1),
legal_address_for(LIST, A2),
A1 \= A2,
not(less(A1, A2)),
not(less(A2, A1)).
ordering_counterexample(LIST, A1, A2) :-
proper_address_for(LIST, A1),
proper_address_for(LIST, A2),
A1 \= A2,
not(less(A1, A2)),
not(less(A2, A1)).
% This predicate checks if a change set is conflicted.
conflicted(LIST) :-
member(X, LIST),
member(A, LIST),
X \= A,
dest(X, Y),
dest(A, B),
Y = B.
% Is a region of the address space deleted by any change in the change
set S?
deleted(A1, A2, S) :-
member(X, S),
operation(X, delete(B, E)),
less_eq(B, A1),
% does provide thorough checking for small examples. (Given the
combinatorics, large
% examples are out of the question.
well_defined_for(LIST) :-
not(ordering_counterexample(LIST, A1, A2)),
not(nil_minimal_counterexample(LIST, A)).
% If there is an element not greater than nil, this predicate
determines its identity.
nil_minimal_counterexample(LIST, A) :-
legal_address_for(LIST, A),
A \= address([], 0),
not(less(address([], 0), A)).
% If there is a pair of addresses that is not properly ordered, this
predicate finds
% them.
ordering_counterexample(LIST, A1, A2) :-
legal_address_for(LIST, A1),
legal_address_for(LIST, A2),
A1 \= A2,
not(less(A1, A2)),
not(less(A2, A1)).
ordering_counterexample(LIST, A1, A2) :-
proper_address_for(LIST, A1),
proper_address_for(LIST, A2),
A1 \= A2,
not(less(A1, A2)),
not(less(A2, A1)).
% This predicate checks if a change set is conflicted.
conflicted(LIST) :-
member(X, LIST),
member(A, LIST),
X \= A,
dest(X, Y),
dest(A, B),
Y = B.
% Is a region of the address space deleted by any change in the change
set S?
deleted(A1, A2, S) :-
member(X, S),
operation(X, delete(B, E)),
less_eq(B, A1),