### Knowledge-Based Systems

Jonathan Lee*

Department of Computer Science and Information Engineering, National Central University, Chungli, Taiwan

Recently, there has been an increasing interest in improving the reliability and quality of AI systems. As a result, a number of approaches to knowledge-based systems modeling have been proposed. However, these approaches are limited in formally verifying the intended functionality and behavior of a knowledge-based system. In this article, we proposed a formal treatment to task structures to formally specify and verify knowledge- based systems modeled using these structures. The specification of a knowledge-based system modeled using task structures has two components: a model specification that describes static properties of the system, and a process specification that characterizes dynamic properties of the system. The static properties of a system are described by two models: a model about domain objects (domain model), and a model about the problem- solving states (state model). The dynamic properties of the system are characterized by (1) using the notion of state transition to explicitly describe what the functionality of a task is, and (2) specifying the sequence of tasks and interactions between tasks (i.e., behavior of a system) using task state expressions (TSE). The task structure extended with the proposed formalism not only provides a basis for detailed functional decomposi- tion with procedure abstraction embedded in, but also facilitates the verification of the intended functionality and behavior of a knowledge-based system.1997 John Wiley &

Sons, Inc.

**I.** **INTRODUCTION**

Recently, there has been an increasing interest in improving the reliability
and quality of AI systems.^{1}As a result, a number of approaches to knowledge-
based systems modeling have been proposed in the Software Engineering and
Artificial Intelligence literature, e.g., Refs. 2 to 8.

In particular, Tsai, Slagle, and their colleagues have conducted an empirical
case study on requirements specifications of knowledge-based systems.^{4,6}These
approaches are important in demonstrating the feasibility of developing specifi-
cations for knowledge-based systems. Meanwhile, Chandrasekaran and several
other researchers have advocated using task structures as a general modeling

*YJLEE@SE01.CSIE.NCU.EDU.TW

INTERNATIONAL JOURNAL OF INTELLIGENT SYSTEMS, VOL. 12, 167–190 (1997)

1997 John Wiley & Sons, Inc. CCC 0884-8173/97/030167-24

approach to knowledge-based systems.^{2,5,9,10}The task structure is a tree of tasks,
methods, and subtasks, which provides a framework for organizing knowledge
in knowledge-based systems in a step-wise refinement fashion. However, these
approaches are limited in formally verifying the intended functionality and behav-
ior of a knowledge-based system.

*Our emphasis in this article is to provide a formal treatment to task structures*
to formally specify and verify knowledge-based systems modeled using these
structures. The specification of a knowledge-based system modeled using task
structures has two components: a model specification that describes static proper-
ties of the system, and a process specification that characterizes dynamic proper-
ties of the system. The static properties of a system are described by two models:

a model about domain objects (domain model), and a model about the problem- solving states (state model). The dynamic properties of the system are character- ized by (1) using the notion of state transition to explicitly describe what the functionality of a task is, and (2) specifying the sequence of tasks and interactions between tasks (i.e., behavior of a system) using task state expressions (TSE).

*TSE extends regular expressions with a task-based composition operator to*
*combine expressions at different levels in a task structure, and a follow operator*
to describe a partial system behavior. TSE can be associated with a task to
describe a global interaction or with a method to specify local task sequencing
in the structure. Progression operators and frame axioms are adopted for con-
structing the descriptions of a state through a TSE to an initial state description
in the context of task structures. The task structure extended with the proposed
formalism not only provides a basis for detailed functional decomposition with
procedure abstraction embedded in, but also facilitates the verification of the
intended functionality and behavior of a knowledge-based system.

In the sequel, we first describe some background work in task structures in
the next section. The formal foundation of task structures is proposed in Section
III. We discuss how to propagate state descriptions in the context of task struc-
tures in Section IV. Verification of specifications modeled using the structures
is presented in Section V. In Section VI, examples based on R1/SOAR^{11}are given
to demonstrate the benefits of our approach. A discussion on the comparison of
the proposed approach to related work is in Section VII. Finally, we summarize
the proposed approach and outlined the plan for our future research.

**II.** **BACKGROUND WORK IN TASK STRUCTURES**

Variations of task structures have been proposed, e.g., Refs. 2, 5, and 12
(Fig. 1). Steels^{5}[see Fig. 1(a)] has proposed work along lines that build on the
notion of tasks and task structures. In his formulation, the task structure is
intended to specify the task/subtask decomposition of a complex task. There is
no explicit notion of alternate methods, that is, the method [M in Fig. 1(a)] is
chosen implicitly in the analysis. The task sequencing relationship in a method
cannot be specified.

In Ref. 2, Chandrasekaran has described a task structure in which we can explicitly identify alternative methods for each tasks in a task structure. A method

**Figure 1.** Variations of task structures.

can set up subtasks, which themselves can be accomplished by various methods.

Only search control knowledge can be described, for instance, the task sequencing relationship between subtasks B and C in Figure 1(b).

Hofsted et al.^{12}has presented a task structure diagram, in which tasks can
be recursively defined in terms of subtasks, and can be decomposed into a
hierarchy of subtasks. Decisions are used if performing a task involves choices
between subtasks [denoted as a circle in Fig. 1(c)]. In task structure diagrams,
sequential execution, iteration, choice, parallelism, and synchronization can be
expressed. For example, task sequencing relationship among subtasks B, C, D,
and E is graphically documented in the task structure diagram, namely, task B
*is executed first, which is followed by the task C and decision d*_{1} in parallel
fashion, and in turn is followed by the choice between task D or E. Similar to
Steel’s approach, there is no explicit notion of alternative methods. The local
task sequencing is expressed using the task structure diagram.

Problems with these approaches can be summarized below:

● cannot verify the consistency of system behaviors due to the lack of a formal foundation of task structures (and tasks);

● lack of a mechanism that can describe partial system behavior, and can fill in the missing detail as the information is available;

● unable to describe global interactions between tasks at different levels.

In the next section, we propose a formal treatment of task structures to formally specify functional specifications and dynamic behaviors of knowledge- based systems modeled using task structures.

**III.** **A FORMAL FOUNDATION OF TASK STRUCTURES**
The specification of a knowledge-based system modeled using task structures
has two components: a model specification that describes static properties of the
system, and a process specification that characterizes dynamic properties of the
system. The static properties of a system are described by two models: a model
about domain objects (domain model), and a model about the problem-solving
states (state model). The dynamic properties of the system are characterized by
(1) using the notion of state transition to explicitly describe what the functionality
of a task is, and (2) specifying the sequence of tasks and interactions between
tasks (i.e., behaviors of a system) using task state expressions (TSE). In this
article we will focus on aspects in the proposed framework that facilitate the
process specification and verification of a knowledge-based system’s functional
requirements. More detailed descriptions about model specifications can be found
in Refs. 8 and 13. In this section, we first formulate the notion of tasks in task
structures, provide a formalism, task state expressions, to describe the relation-
ships among tasks, methods, and subtasks, and conclude with the specifications
of tasks and methods.

**A.** **Formal Semantics of Tasks in Task Structures**

*To explicitly specify what a task is in a task structure, a task is treated as*
(1) a state-transition which can take one state to another through a sequence of
intermediate states, and (2) a functional unit that can be specified by using
preconditions, protections, and postconditions, which are partial state descrip-
tions about the state before, during, and after performing the task. State transition
model is thus adopted for the purpose of formulating and analyzing the proposed
specification methodology. In the general form of the model (e.g., Ref. 14), the
world is viewed as being in one of a potentially infinite number of states. The
effect of a task is to cause the world to make a transition from one state to
another. Each task is therefore modeled by a set of triple*kb, dˆ*

*, al where b and*
*a are states, and dˆ*

*is a sequence of states, b being the ‘‘before state,’’ dˆ*
being
*the ‘‘during state,’’ and a being the ‘‘after state.’’*

DEFINITION *1 (State Transition): A task T is defined as a set of tripleskb, dˆ*
*, al,*
*where b and a denote the state before and after an invocation of T, and dˆ*

*denotes*
*the sequence of states during the invocation of T.*

*Formulas in first-order logic are used for state descriptions. The precondition*
of a task is a condition (i.e., a formula) that needs to be true for all states before
the task. The rigid postcondition of a task is a condition that is true for all states
after the task. The protection of a task is a condition that needs to be held before,
during, and after the execution of the task. These are formally defined below.

DEFINITION*2 (Functional Specification): Let a task T be a set of tripleskb, dˆ*
*,al.*

*1. A formulaw is a precondition of a task T, denoted as B**T**, if and only ifw is true*
*in state b, for every triplekb, dˆ*

*, al [ T.*

*2. A formulaw is a protection of a task T, denoted as P**T**, if and only if for every*
*triplekb, dˆ*

*, al [ T,w is true in state b, w is true in state sequence dˆ*

*, andw is true*
*in state a.*

*3. A formulaw is a rigid postcondition of a task T, denoted as R**T**, if and only if for*
*everykb, dˆ*

*, al [ T,w is true in state a.*

*4. A formulaw is a soft postcondition of a task T, denoted as S**T**, if and only if for*
*everykb, dˆ*

*, al [ T, the degree to whichw is true in state a is a real number [ [0, 1].*

**B.** **Task State Expression**

*Task state expression (TSE), based on regular expressions, is to describe the*
dynamic behavior of a system modeled using task structures. Regular expression
has been used in AI planning to represent the procedural knowledge (e.g., Ref.

15) and in software engineering to describe the behavior of a software system (e.g., Ref. 16). A TSE is an expression that defines (1) the desirable sequence of tasks that are expected to have processed before a given task, and (2) interactions between tasks at different levels. The notion of conditional expression is also adopted in TSE. We formally define TSE below.

DEFINITION*3 (Task State Expression). The task state expression, E , over a set of*
*tasks, I* *5 hT*1*, T*2*, . . . , T**n**j, is defined as follows:*

1. *« is a task state expression, where « stands for null.*

*2. For each task T[ T , (T) is a task state expression.*

*3. If E**i**and E**j**are task state expressions, then (E**i,**E**j**) is a task state expressions, where*

*‘‘,’’ denotes immediately follow.*

*4. For each expression E ,* *bE is a task state expression, where b is a well-formed*
*formula to be attached to a TSE, E , to represent the conditional branching. For a*
*TSE, E , ‘‘b*1*E*1~ b1*E*2. . .~ b*n**E**n**’’ means ‘‘If*b1*then E*1*else if*b2*then E*2*. . . else*
*if*b*n**then E**n**’’ where~ denotes selection, and b*1,b2, . . . ,b*n**are mutually exclusive.*

*5. For each expression E , [E ] is a task state expression and is a short hand notation*
*for (« ~ E), where ‘‘[ ]’’ denotes optional.*

*6. If E**i**and E**j* *are task state expressions, then (bE**i**)* and (E**i*, *bE**j**)* are task state*
*expressions, where ‘‘*’’ denotes iteration and ‘‘b’’ is an iteration condition.*

*7. If E**i**and E**j**are task state expressions, then (E**i**; E**j**) are task state expressions, where*

*‘‘i’’ denotes follow.*

Graphical notations of TSE operators in a task structure diagram are shown
*in Figure 2. The relationship between subtasks B and C of method M*1 is a
*sequential relationship [that is, (B, C)]. Selectional relationship is illustrated*
*using the relationship between the subtasks of method M*_{2}, denoted by conditions
b1,b2, and a ‘‘n’’ within a rectangle [e.g., (b1*D* ~ b2*E)]. As for iteration, there*
are two cases: (1) the iteration condition is associated with the whole expression
(namely,b3*(F, G)]; and (2) the iteration condition is associated with a subtask*
*of its method [e.g., (F,*b4*G)]. We call the relationship between task F and B a*
global interaction (denoted using a dotted line), because the interaction is be-
tween tasks at different levels. This kind of relationship can be expressed using
*a follow operator [e.g., (F; B)].*

**Figure 2.** Dynamic behaviors in a task structure.

A TSE represents a collection of possible sequences of task invocations,
*referred to as task sequences. More formally, the semantics of a TSE over T is*
*defined by a mapping to S , which is the set of all possible task sequences for*
*tasks in T . The convention of viewing a conditional test as a task is also adopted,*^{17}
denoted asb?. b? is a special control flow task that is invoked only when b is
tested to be true. Similarly, ¬b? is another special control flow task that is
invoked only when ¬b is tested to be true. The mapping function between a
TSE and its corresponding task sequences is defined as follows:

DEFINITION*4. Let E*1*, E*2*be TSEs over T , T[ T and b be a well-formed formula.*

*G is a function that maps a TSE to a subset of S such that*
1. *G(«) 5 hhj, where h denotes the empty task sequence.*

2. *G(T) 5 hktlj, where t denotes an invocation of T and k l denotes a task sequence.*

3. *G(E*1*, E*2)*5 hs*1*n s*2*us*1*[ G(E*1)*` s*2*[ G(E*2)j, where n stands for concatenation.

4. *G([E*1])*5 hhj < G[(E*1)].

5. G(b1*E*1~ b2*E*2)5 G(b1*?, E*1)< G(b2*?, E*2).

6. *G((bE*1)*)*5 G((b?, E*1)*, (¬b?, «))

*5 hs n*¬b? n hus [ G((b?, E1)*)j,

*whereG((b?, E*1)*)5 <^{y}*i51*G* ^{i}*(b?, E1

*), and*G

*(b?, E1)*

^{i}*5 hs*1

*n s*2

*n . . . n s*

*i*

*us*

*j*[ G(b?,

*E*1), 1

*# j # ij*

7. *G(E*1*; E*2)*5 hs*1*n s*3*n s*2*us*1*[ G(E*1)*` s*2*[ G(E*2)*` s*3*[ S ].*

A TSE can be described at either the task level (a global TSE) or at the
*method level (a local TSE). In Figure 2, E**F**5 (F; B) and E**M*_{2}5 (b1*D* ~ b2*E)*
are examples of global and local TSEs, respectively. A TSE at the task level is
used to document global interactions between the current task and tasks at
different levels that require special attentions in implementing and testing the
system. A TSE at the method level documents the local control flow between
subtasks of the method. To specify a global interaction, a global TSE often uses
the ‘‘follow’’ operator (‘‘;’’) to describe a set of partial task sequences. In contrast,
a local TSE, which typically does not contain the ‘‘follow’’ operator, completely
describes the control flow among the method’s subtasks. A TSE that does not
contain the ‘‘follow’’ operator is called a complete TSE; otherwise, it is called
a partial TSE.

There is another important difference between the semantics of the global
*TSE and the local TSE. A global TSE describes expected system behavior when*
*the associated task is invoked. This property plays an important role in combining*
TSE’s at different levels. The current task to which a global TSE is associated
is denoted by ‘‘1’’. The semantics of the global TSE implies that it is meaningless
to use optional, conditional, and selection operators for a task to which the task
level TSE is associated, and therefore TSEs such as ([1]), (b1), and (1 ~ T*i*)
are invalid TSEs at the task level.

**C.** **Composition Operators**

Multiple TSEs often need to be combined to obtain a global view of the
system’s behavior from pieces of local behavior specifications. To achieve this,
*a composition operator is developed for combining two TSEs with a designated*
*task T (called task-based composition operator), denoted as*%*T*. The semantics
of composing two TSEs is defined through the corresponding set of task se-
quences. To compose two task sequences on a designated task invocation, de-
*noted as (s*1 %*t* *s*2), is defined by examining the relationship between the two
sequences. We have identified three types of relationship between any two
task sequences.

*(a) Two task sequences may share a common subsequence containing an invocation*
of a designated task T [see Fig. 3(a)].

*(b) Two task sequences are irrelevant w.r.t. a designated task T, if at least one task*
sequence does not contain an invocation of T [see Fig. 3(b)].

*(c) Two task sequences, s*1*and s*2*, are said to have a conflicting subsequence w.r.t.*

a designated task T, if (1) the task sequences contain the invocation of T, (2)
*there exists a predecessor (or successor) of T in s*1that is different from that in
*s*2(which is called a conflicting predecessor or successor), and (3) the conflicting

**Figure 3.** Relationships between any two task sequences.

predecessor (or successor) is not mapped to by a ‘‘follow’’ operator. Note that condition (3) is necessary in that, based on the definition of the follow operator, we can always find a conflicting predecessor (or successor) when composing a complete TSE with a partial one [see Fig. 3(c)].

DEFINITION*5 (Composing Two Task Sequences). Suppose s*_{1}*and s*_{2}*are two task*
*sequences. The composition of s*_{1}*and s*_{2}*on an invocation of a designated task T,*
*denoted as (s*_{1}%*t* *s*_{2}*), is defined as follows:*

*● If s*1*and s*2*are sharing a common subsequence on an invocation of T, then*
*if s*1*5 s9*1*n a and s*2*5 a n s9*2*then s*1%*t**s*2*5 s9*1*n a n s9*2

*else if s*1*5 s9*1*n as0*1*and s*2*5 a then s*1%*t**s*2*5 s9*1*n a n s0*2

*● If s*1*and s*2*are irrelevant, then s*1%*t**s*2*5 s*1<*s*2.

*● If s*1*and s*2*have a conflicting subsequence containing an invocation of T, then s*1

%*t**s*25 h.

*The semantics of composing two TSEs conditioned on a designated task T,*
is defined through its corresponding set of task sequences,*G(E*1%*T**E*2). That is,
*we can take a task sequence from E*1and compose it with all task sequences in

*E*2by taking the union, and repeat the same process until all task sequences in
*E*1are considered. This is formally defined below.

DEFINITION *6 (Composing Two TSEs). Let E*1 *and E*2 *be two TSEs over T .*
*Suppose T is a task in T . The semantics of composing E*1*and E*2*conditioned on*
*the designated task T, denoted as E*1%*T**E*2*, is defined as follows:*

*G(E*1%*T**E*2)5;*s*_{1}[G(

## <

*E*

_{1}),;

*s*

_{2}[G(

*E*

_{2})

*(s*1%*t**s*2)

It is trivial, from Definition 6, to show that the composition operator has the following properties:

*● commutative: E*1%*T**E*2*5 E*2%*T**E*1.

*● associative: (E*1%*T**E*2)%*T**E*3*5 E*1*%T**(E*2%*T**E*3).

However, not all TSEs in task structures are eligible for composition. There
*are two factors that affect the composability of TSEs: the conflicting task sequence*
and the follow operator. Intuitively, if there exists a conflicting task sequence in
the to-be-composed TSEs, then we should not compose the TSEs. However, to
compose a partial TSE with a complete TSE, we need to ensure that there does
not exist a task sequence in the complete TSE that is conflicting with every
possible task sequences of the partial TSE. A formal definition of composability
is described below.

DEFINITION*7 (Composability). Two TSEs, E*1*and E*2*, are not composable condi-*
*tioned on a designated task T, iff's*1 *[ G(E*1),*;s*2*[ G(E*2*), such that s*1*and s*2

*are conflicting w.r.t. T.*

The following theorems for composing TSEs follow from Definition 4 and 6.†

THEOREM*1. Let E and E**T**be two TSEs over T , and T be a task in T . If E does*
*not contain any invocation of T inG(E**T**), then E* %*T**E**T**5 E ~ E**T*.

THEOREM*2. Let E*1*, E*2*, and E**T**be three TSEs over T . E**T**denotes a TSE in which*
*T appears. (E*1*~ E*2)%*T**E**T**5 (E*1%*T*)*~ (E*2%*T**E**T*).

THEOREM *3. Let E*1 *and E*2 *be two TSEs over T , E*1 *5 (a, T, b(c*1, c2*)), and*
*E*2*5 (T, b(c*1;*g)), where a, c*1,c2*andg are TSEs, and b is a condition. E*1%*T*

*E*2*5 (a, T, b(c*1,c2;g)).

To summarize, there are two important characteristics of the task-based composition operator. First, to prevent any arbitrary composition, the composi- tion is conditioned on a designated task to focus the attention on tasks that are

†All proofs of theorems can be found in Appendix A.

Task: Model:

. Model Specification: . Parent Task:

- Domain Model: . Guard Conditions:

- State Model: . Subtasks:

. Process Specification: . TSE:

- TSE:

- Precondition:

- Postcondition:

**Figure 4.** Task and method specification templates.

related to or interacted with the designated task. Second, combining a complete TSE with a partial one will help to fill in some of the missing details by fusing multiple pieces of behavioral specification.

As an illustration of the composition of TSEs, let us consider the following
*example. Suppose E**M**5 (T*1*, [T*3*]), and E**T*_{3}*5 (1; T*4).

*E**M*%*T*_{3}*E**T*_{3}*5 ((T*1)*~ (T*1*, T*3))%*T*_{3}*(T*3*; T*4) (1)
*5 (((T*1)%*T*_{3}*(T*_{3}*; T*_{4}))*~ ((T*1*, T*_{3})%*T*_{3}*(T*_{3}*; T*_{4}))) (2)
*5 ((T*1)*~ (T*3*; T*_{4})*~ (T*1*, T*_{3}*; T*_{4})) (3)

*In this example, the global TSE is associated with T*3*. However, T*3 is an
*optional task in its parent method. To compose E**M**and E**T*_{3}, from Definition 4,
*we can transform E**M*into an equivalent TSE that has two components: one that
*always invokes T*3*, the other that does not invoke T*3at all. Based on Theorem
2, we can derive Eq. (2). Equation (3) follows directly from Theorem 1 and
Definition 6.

Templates for tasks and methods specifications are shown in Figure 4. A
task can be described using the triple*kprecondition, protection, postconditionl,*
and the relationship between the task and tasks at different levels is captured
by a global TSE. A task in a task structure can be refined into a set of methods
that can accomplish the task. Each method can be further refined by specifying
subtasks involved and sequencing relationship between subtasks using a local
TSE. The specifications of tasks and methods are defined below.

DEFINITION*8 (Task Specification). A specification of a task T is a tuplekC**T**, E**T*l,
*where C**T**is a triplekB**T**, P**T**, R**T**~ (R**T**` S**T*)l, and E*T**is a task state expression*
*involving tasks which have global interaction with T.*

DEFINITION *9 (Method Specification). A method specification of a task T is a*
*quadruplekT, g, ST, E**M**l, where g is a formula describing the guard condition*
*under which the method is applicable, S T is a collection of subtasks, and E**M**is*
*a TSE involving subtasks in S T.*

**IV.** **COMPUTING STATE DESCRIPTIONS IN TASK STRUCTURES**
In software specifications, it is desirable to compute the description of a
state after the application of a transition.^{18}Similarly, researchers in AI planning
are concerned about synthesizing a plan (that is, a sequence of actions) which
involves constructing a state description after executing an action. Both software
*specifications and AI planning share a similar problem: How to keep track of*
*what has not been changed? (This is the so-called frame problem*^{19}.) The frame
problem and its partial solutions are introduced in the next section. Section B
elaborates on the proposed approach to the frame problem in the context of
task structures.

**A.** **Frame Problem in Software Specifications**

In AI planning, frame axioms have been used to describe what has not been
changed after the performance of an action. However, the problem arises when
the number of frame axioms increases rapidly with the complexity of the applica-
tion. Several partial solutions have been proposed. Fikes and Nilsson used the
notion of differences, as well as ideas from the situation calculus to make the
assumption that the initial world model would only be changed by a set of
additions to, and deletions from, the statements modeling the world state—every-
thing else remained unchanged.^{20} This assumption is sometimes called the
STRIPS assumption. Hayes proposed using causal connections as a frame rule
to the frame problem.^{19}The assumption is that if a term (or a nonlogical symbol)
is not connected to an action, then any change to the action does not affect
the term.

In software specifications, it is sometimes necessary to express explicitly the
*fact that certain variables do not change value (or state) due to the performance*
of a task.^{21,22}ASLAN^{21}provides four procedural operators: NoChange, ALTerna-
tive, Conditional, and Become, to explicitly specify unmentioned variables which
are assumed not to have changed; meanwhile, the notationQ in Z has been used
to denote that any variable followed by theQ will not change value, and J is
used to indicate that any state space followed byJ will not change. Four types
of solutions to the frame problem are identified below:‡

● Domain-independent approaches: the solution is designed to be applicable to a wide variety of domains, for example, STRIPS assumption and the causal connec- tion frame rule.

● Domain-independent, if-needed-basis approaches: a frame axiom is generated by the system on a if-needed-basis. A typical example of this approach is the NoChange operator in ASLAN, which is generated if the correctness of a specification cannot be proved due to the missing of values for variables.

● Application-specific approaches: frame axioms are tightly related to the application,
and therefore, it is necessary for users to explicitly specify what will remain unal-
tered, for instance, the notion of invariant in software specifications such as Z.^{22}

● Operator-specific approaches: the solution is tied to a specific implementation of

‡A similar classification scheme can be found in Ref. 23.

a specification language, and is only applicable to that particular language. The procedural operators in ASLAN are examples of this category.

To compute the description of a state involves not only the propagation of what has not been changed, but also the progression of what has been changed.

Rosenschein’s progression operator^{24}and Waldinger’s regression operator^{25}are
two similar approaches to only specifying what has been changed using a tuple
*kprecondition, postconditionl in the state before and after an action. A progres-*
sion operator is a function that maps conditions that are true immediately before
a task (called before-state description) to conditions that are true immediately
after the task (called after-state description), which is formally defined below.

DEFINITION*10 (Progression Operator). A progression operator, denoted as /; for*
*T is a function mapping from formulas to formulas, such that for every triplekb,*
*dˆ*

*, al [ T, if*w*is true in state b, then*w*/T is true in state a.*

*;kb, dˆ*

*, al [ T, b u5*w^{⇒}* ^{a}*u5 w

^{/T}In the proposed framework, for the purpose of verification, it is desirable to compute the description of a state that is obtained through a TSE to an initial state description, which is addressed in the next section.

**B.** **Computing State Descriptions**

As was noted by Borgida et al.^{23} that the frame problem is still an open
issue and that it is likely no single general solution exists. In this section, the
notions of progression operator, default rule, and frame axioms are introduced
to address this problem in the context of task structures.

To extend the progression operator in the context of task structures, we first assume the description of a state is in a disjunctive normal form. An assump- tion about the forms of the precondition and the postcondition of a task is also made, that is, the precondition is a conjunction of literals; while the postcondition assumes a disjunctive normal form.

Second, the notion of default rule proposed by Reiter^{26} and frame axioms
advocated by Hayes^{19} are incorporated into the semantics of the progression
operator to specify state descriptions that remain unchanged after performing a
task. The default rule and frame axioms are used to describe state descriptions
that remain unaltered after performing a task. In default logic, unless there is
knowledge to the contrary, we assume what is assumed to be true in the before
state is also assumed to be true in the after state. Thus, the default rule is
*formulated as: a literal in the description of a state will remain intact if the literal*
*is not contradictory to the postcondition of the task. This is formally defined below.*

DEFINITION *11. Let the state description*w*i**to a task T in a specification be in a*
*disjunctive normal form:*w5 (w1~w2~ ? ? ? ~w*n**), where*w*i**in*w*is a conjunction*
*of literals:*w*i**5 (l*1*` l*2*` . . . ` l**n**), and*w*i**R B**T*,w*i**/T5 R**T*`w*j**, where*w*j**is*
*a conjunction of literals and l**i**in*w*i**such that l**i**is not contradictory to R**T*.

Several features in the proposed framework facilitate the formulation of frame axioms: domain model, state model, and protections. Both the value of a variable and the state of an object in the model specification of a task can be changed after performing the task, which is analogous to the value of a variable (or a state variable) in conventional software specifications. Most software speci- fications methods use a variable with a prime (that is,9) to represent the old value of the variable and a variable without the prime for new value of the variable, which is a convention adopted in the proposed framework. The same approach is used for representing the change of status for a state variable in conventional software specifications. However, in the proposed framework, the notion of state objects in the state model, represented using either a proposition or a predicate, is used to reflect the change of status for an object. Therefore, predicates in the domain model of a task should never be changed after the task.

From the definition of protections in the functional specification of a task, the predicates in the protection should remain intact after the execution of the task.

Based on the above discussion, the following lemma can be derived.

LEMMA*1. Let D be the domain model of a specification and the state description*
w*i**to a task T in the specification be in a disjunctive normal form:*w5 (w1~w2

~ . . . ~w*n**), where*w*i**in* w *is a conjunction of literals:*w*i**5 (l*1 *` l*2` . . . `
*l**n**), and*w*i**R B**T*,w*i**/T5 R**T*`w*j**, where*w*j**is a conjunction of literals and l**i**in*
w*i**in* w*i**such that l**i**satisfies any of the following:*

*1. l**i**is a domain model predicate.*

*2. l**i**is a predicate in the protection of T.*

Third, since the proposed framework adopts the notion of task structures
*for functional decomposition, the progression is only performed within each task*
(that is, the task, its methods, subtasks of the methods, and tasks related through
global interactions). In another word, the initial state description is the conjunct
of the precondition of the task and the guard condition of the task’s method,
and the state descriptions are progressed through the composed TSE of the
task’s method TSE and the TSE of any high level task that has global interactions
with any task in the method.§ For example, in Figure 2, to propagate through
*the task D is to progress through the composed TSE: E**M*_{3} %*F* *E**B* *with B**D* `
b*M*_{3}as the initial state description.

To progress a state description through an immediate follow operator (‘‘,’’)
in a TSE, there are two conditions which need to be satisfied: (1) the state
*description is in a disjunctive normal form, and (2) the precondition of a task T*
that immediately follows the operator can be derived from every disjunct in the
state description. The result of the progression through the immediately follow
operator will be equivalent to the disjunction of applying the progression operator

§To make it consistent in the presentation, ‘‘/’’ is used to represent both the progres- sion operator through a task and a TSE.

*to each individual disjunct over the task T. This is formally described using the*
following theorem.

THEOREM*4. Suppose the initial state description*w*to a TSE E is in a disjunctive*
*normal form:*w5 (w1~w2~ . . . ~w*n**), where*w*i**in*w*is a conjunction of literals.*

*If E* *5 («, T) and ;i*w*i**R B**T**, then (*w1,~ . . . ~w*n**)/E* 5w1*/T*~ . . . w*n**/T.*

To progress a state description through a selection operator (‘‘~’’) in a TSE,
several conditions need to be satisfied: (1) the state description is in a disjunctive
normal form, (2) at least one disjunct in the state description can deduce the
*precondition of the task T (i.e., B**T*) that is used with the selection operator.

The result of the progression is a disjunction of applying the progression operator
*over T to those disjuncts that can derive B**T*, and applying the progression
*operator to those disjunctions that cannot derive B**T*.

THEOREM*5. Suppose the initial state description*w*to a TSE E is in a disjunctive*
*normal form:*w5 (w1~w2~ . . . ~w*n**), where*w*i**in*w*is a conjunction of literals.*

*E* *5 (T*1*~ T*2)

*If* w 5 w9 ~ w*0 where*w*9 and* w*0 are in disjunctive normal form, such that*

;w*i**in*w*9,*w*i**R B**T*_{1}*, and*;w*j**in*w*0,*w*j**R B**T2**, then (*w9 ~w*0)/ E 5*w*9/T*1~ (w*0)/T*2.
Based on the above discussion, the following algorithm will compute the
*state description through a TSE E to an initial state description*w. A specification
is said to be weakly inconsistent if a consistency condition cannot be proved;

meanwhile, if a consistency condition can be disproved, then the specification is said to be strongly inconsistent (the detail of levels of inconsistency is described in the next section).

ALGORITHM*1 (Progression Algorithm for a TSE). Assume that the initial state*
*description*w*to a TSE E is in disjunctive normal form:*w5 (w1 ~w2~ . . . ~
w*n**), where*w*i**in*w*is a conjunction of literals. Domain model predicates are denoted*
*as*w*D*.

*1. E* *5 («, T)*

*Case 1: If;i*w*i**R B**T**, then (*w1~ . . . ~w*n**)/E*5w1*/T*~ . . . ~w*n**/T.*

*Case 2: If*'w*i**such that*w*i*R*y B**T**, then weakly inconsistent.*

*Case 3: If*'w*i**such that*w*i*R¬B*T**, then strongly inconsistent.*

*2. E* *5 (T*1*~ T*2)

*Case 1: If*w5w9 ~w*0 where*w*9 and*w*0 are in disjunctive normal form,*
*such that* ;w*i* *in* w*9,*w*i**R B**T1**, and* ;w*j**in* d*0,*w*j* *R B**T*_{2}*, then (*w9 ~
w*0)/E 5*w*9/T*1~w*0/T*2.

*Case 2: if*'yw*i**in*w* ^{such that}*w

*i*

*R B*

*T*

_{1}

*or*w

*i*

*R B*

*T*

_{2}

*, then weakly incon-*

*sistent.*

*Case 3: If*'w*i**in*w* ^{such that}*w

*i*R¬B

*T*

_{1}

*and*w

*i*

*R B*

*T*

_{2}

*, then strongly incon-*

*sistent.*

*3. E* *5 («; T)*

w*/E* *5 R**T*`w*D**` P**T*`w*9, where*w*9 is the state description constructed*
*by the expression performed immediately before T.*

*4. E* *5 (bT)**

w*/E* 5¬b `w*D**` P**T*`w*9, where*w*9 is the state description propagated*
*immediately before exiting the iteration.*

**V.** **VERIFICATION OF SPECIFICATIONS**

The verification of a specification is important because it helps early detec- tion of errors in the software life cycle to produce an adequate specification, thus eliminating possible design failures and reducing product costs. The proposed framework provides two levels of inconsistency checking in a single layer: strong and weak inconsistency. A system specification is weakly inconsistent if its consis- tency cannot be proved. On the other hand, a system specification is strongly inconsistent if its consistency can be disproved. The proposed framework also checks for if a refinement is consistent by comparing the specificity of conditions at the high layer to that of the low layer. Types of faults that could result in an inconsistent process specification include protection violation, precondition violation, postcondition violation, and incorrect TSEs. Missing methods will result in incompleteness in the specification.

A specification of a task or a method of a system is consistent if (1) the precondition of a task in the TSE of a task or a method can be deduced from the state description before performing the task; (2) the postcondition of the task can be deduced from the description of the state after performing the task;

*and (3) the protection of T can be deduced from state descriptions before, after,*
and during performing the task.

Thus, a method specification of a task is weakly inconsistent if (1) the precondition of a task in the TSE of the method cannot always be deduced to be true from the state description after the task: (2) the postcondition of the task cannot always be deduced to be true from the state description before the task; and (3) the protection of the task cannot always be deduced to be true from the state description before, after, or during the task. In contrast, a method specification of a task is strongly inconsistent if (1) the precondition of a task in the TSE of the method can sometimes be proved to be false from the state description after the task; (2) the postcondition of the task can sometimes be proved to be false from the state description before the task; and (3) the protection of the task can sometimes be proved to be false from the state description before, after, or during the task.

The consistent refinement checking is performed between adjacent levels of a task and its methods. The mechanism for verifying the consistency is to check for if a refinement is consistent by comparing the specificity of conditions at the high level to that of the low one.

DEFINITION *12 (Specificity of Conditions). A condition C*_{1} *is exclusively more*
*specific, denoted asa, than condition C*2*if and only if for all states s, if s satisfies*
*C*_{1}*, then s satisfies C*_{2}*, but not vice versa (i.e., they are not equivalent).*

*C*1*a C*2⇔(;s, s u5 C1⇒*su5 C*2)` ¬(;s, s u5 C2⇒*su5 C*1)

DEFINITION *13 (Consistent Refinement). A refinement of a task T is consistent*
*with T’s specification, if and only if the collection of state transitionkb, dˆ*

*, al of*
*T’s methods is a subset of the collection of T’s state transitionkb, dˆ*

*, al [ T.*

THEOREM*6 (Inconsistent Refinement). LetkC**T**, E**T**l be a task specification of T,*
*andkT, g, S T, E**M**l a method specification M of T. M is an inconsistent refinement*
*of T, if one of the following holds:*

*1. B**T*s*y B**M*.
*2. P**T*s*y P**M*.
*3. R**T*s*y R**M*.

*4. R**T**` S**T*s*y R**M**` S**M*.

THEOREM *7 (Protection Violation). A refinement of T is inconsistent, if* w ^{is}*protected during task T, there exists a subtask T9 of a method M in T’s refinement*
*such that the rigid postconditions of T9 can deduce*¬w^{.}

DEFINITION*14 (Complete Refinement). A refinement of a task T is complete with*
*T’s specification, if and only if the collection of the before states of T’s method*
*specifications is equivalent to the collection of the before states of T.*

The verification of the process specification starts from the highest level task, and focuses one task at a time.

ALGORITHM*2. To verify a task, there are two major steps involved:*

*1. The specification of a task T is compared with the method that contains*
*T (called T’s parent method) and other subtasks in the method to prove*
*or disprove T’s precondition using the resolution algorithm.*

*2. The specification of a task T is compared with those methods (and their*
*subtasks) that accomplish T (i.e., T’s child methods) for consistency and*
*completeness checking.*

**(a) The specification of a T’s method is consistent with T if**

*i. the description of the state prior to executing the method, referred*
*to as the before state description, is semantically more specific than*
*T’s precondition,*

*ii. the description of the state after executing the method, referred to as*
*the after state description, is more specific than T’s rigid postcondition,*
*iii. the protection of T is not violated by any subtasks of T.*

**(b) The specification of T’s methods is considered complete if the union***of their before state descriptions is equivalent to T’s precondition.*

*Task: configure modules*

● Model Specification:

— Domain Model: (omitted)

— State Model:

* A moduled backplane is a backplane that 1) has as many modules as possible been placed in, and 2) satisfies the constraint of maintaining the optimal ordering of modules configured into the backplane.

● Process Specification:

— Precondition: There exists a current backplane, and a sequence of modules.

— Protection: The optimal ordering of modules should be maintained (inherited).

— Postcondition:

* (rigid) The chosen backplane is a moduled backplane.

**Figure 5.** Configure modules.

**VI.** **AN EXAMPLE**

Based on an original implementation and documentation of R1/SOAR, the
reimplementation of a major portion of the well-known computer configuration
expert system R1,^{11} we have constructed, in a reverse engineering fashion, a
specification for R1/SOAR to evaluate the proposed framework.

R1/SOAR focuses on the unibus configuration task of the entire configura- tion task of R1. The problem is given a customer’s order, place the modules on the order into backplanes, and the backplanes into boxes on the correct unibus.

The backplanes need to be cabled together, and the panel space allocated when required by the modules. If the containers on order are not sufficient to hold the modules, additional containers must be ordered.

The following example is from a subset of the task-based specifications of
*R1/SOAR. Two major tasks of concern in this example are configure modules*
*and configure a module. The functionality of the task configure modules is to*
configure as many modules as possible into the current backplane while main-
taining the optimal ordering. This is achieved by iterating between two subtasks:

*(1) configure a module, which attempts to configure the current module into the*
*current backplane, and (2) obtain the next module, which gets an ordered module*
that follows the current module in the optimal ordering.

One of the errors that a knowledge engineer is likely to make is about the
situation when the current module fails to be configured into the current back-
*plane. A correct specification should indicate that obtain the next module should*
be skipped under the situation, since we have not finished configuring the current
module yet. It is also desirable to indicate that if the current module cannot be
configured into the current backplane, the system should later find a backplane
suitable for the current module before configuring the next module. The specifi-
cations for the tasks and methods relevant to this example are shown in Figures
5, 6, and 7. We discuss the state model, functional specification, and behavioral
specification relevant to the example below, and show how the common error
mentioned above can be detected by the verification algorithm.

*Functional specification: An example of protections in R1/SOAR is that the*
optimal ordering in which modules are configured should be maintained in the

Method:

● Parent Task: Configure Modules

● Guard Condition: TRUE

● Subtasks:

*— T*1: configure a module.

*— T*2: obtain the next module.

*● TSE: (T*1*, [T*2])*

**Figure 6.** A method of the task configure modules.

*task unassigned backplane. Consequently, both tasks inherit the protection from*
*the parent task unassigned backplane. The postcondition of the subtask configure*
*a module is a conjunction of two conditions, corresponding to the two possible*
outcomes that the task succeeds or fails in configuring the current module into
the current backplane.

*Behavioral specification: The rational underlying TSEs in this example is*
that if the current module and current backplane are incompatible, then we
*should latter find a backplane suitable for the current module and not to try to*
configure another module using the current backplane, because doing so will
violate the protection to maintain the optimal ordering of modules. From the
*local TSE of the method, E**M**5 (T*1*, [T*2*])*, and the global TSE of T*1*, E*T_{1}5 (1;

*[T*3]) (see Fig. 7), the result of the composition can be derived as follows:

*E**M*%*T*_{1}*E**T*_{1}*5 ((T*1*, [T*_{2}])*%*T*_{1}*(T*_{1}*; [T*_{3}]) (4)
*5 ((T*1*, [T*_{2}*])*; [T*_{3}]) (5)

*Task: configure a module*

● Model Specification:

— Domain Model: (omitted)

— State Model:

* A current module is said to be compatible with the current backplane if 1. The current module’s unibus load is less or equal to the univus load left.

2. The current module’s pin type is the same as the current backplane’s pin type.

3. The current module is a kmc11 and the backplane is either 4-slot or 9-slot.

4. Modules’ power drawn for some type of power is less or equal to the available power of that type.

5. There is enough room for the current module in the backplane.

● Process Specification:

— TSE: (*1;[T*3: find a backplane suitable for current module])

— Precondition: There exists a current module, and a current backplane.

— Protection: The optimal ordering of module should be maintained (inherited).

— Postconditions (disjunctive):

* (rigid)

1. The current module is compatible with the current backplane and is configured into the current backplane. Or,

2. The current module is not compatible with the current backplane and the current backplane is a moduled backplane.

**Figure 7.** Configure a module.

*Verification: If the TSE of the method were (T*1*, T*2)*, a strong inconsistency
*will be detected by the verification algorithm because the postcondition of con-*
*figure a module can be formally expressed using the following logic formula:*

*configured(current2 module)*

*~ incompatible(current 2 module, current 2 backplane)*
*Invoking the sequence, (. . . T*2*, T*1. . .), when the current module is incompati-
ble with the current backplane leads to configuring the next module before
configuring the current one. Hence, two strong inconsistencies can be detected:

*(1) the precondition of the task obtain the next module, which states that the*
current module should have been configured, can be violated, and (2) the protec-
tion that the optimal ordering of modules should be maintained can also be vio-
lated.

**VII.** **RELATED WORK**

We briefly compare our methodology with major alternative specification methodologies for knowledge-based systems below.

● Zualkernan and Tsai have developed two specification methodologies for expert
systems: an object-oriented methodology, and a knowledge-model methodology.^{6}
The object-oriented methodology first establishes the object class for specifying
instances of each of the expert activity involved, which is followed by the definition
of the methods for each class, and then the instantiation of class instances. The
knowledge-model methodology describes the concept structures and the goal struc-
tures that are required to solve the problem. Both methodologies provide a top–

down approach and have been demonstrated for a heuristic classification system.

Verification and validation are performed through the interaction with experts.

Compared to our approach, both methodologies offer two benefits: (1) the specifi- cation is executable, and (2) the methodologies are easier to be applied to the heuristic classification type expert systems.

● Slagle has used conceptual graphs for specifying a heuristic classification expert
system.^{4}His approach begins with type definitions, identifies the high-level lines
of reasoning focused on a few concepts, construct implications, facts, type lattice,
and canonical graphs. Like Zualkernan and Tsai’s work, Slagle’s methodology is
suitable for heuristic classification type systems, whose knowledge can be specified
by constructing an inference network that relates pieces of evidence to hypotheses.

● A problem space approach to expert system specification has been proposed by
Yost and Newell.^{27}The approach is designed specifically for the SOAR architecture.

It is difficult to see how the methodology can be applied to other AI architectures.

Furthermore, verification of the specification has not been demonstrated.

The proposed approach offers two important advantages: (1) It provides a solid automatic verification capability. (2) It provides a detailed functional decomposi- tion technique.

**VIII.** **CONCLUSION**

In this article, the formal foundation for task structures has been proposed
to formulate two major features in process specification: state-transition and
process refinement. The general form of state-transition model^{24,28}is thus adopted

for the purpose of formulating and analyzing the notion of tasks in the structures.

The notion of task structure (i.e., task/method/subtask) is formalized for the analysis of task process refinement. Task state expressions, based on regular expressions, are used to describe expected behavior specifications. Progression operators and frame axioms are adopted for constructing the description of a state through a TSE to an initial state description. Levels of inconsistency: strong and weak, have been identified. The formalism provided by the framework facilitates the verification of specifications. Verification for consistency and com- pleteness is performed for pieces of the specification within one abstraction level or between multiple levels based upon their formal semantics.

Our approach offers several important benefits for specifying knowledge- based systems. First, the incorporation of task structures provides a detailed functional decomposition technique for organizing and refining functional and behavioral specifications of a knowledge-based system. Second, the use of TSEs can assist not only in documenting the expected control flow and module interac- tions, but also in verifying that the behavioral specification is consistent with the system’s functional specification. Third, the verification algorithm is based on its well-defined formal foundation, and is achieved by centering around one func- tional unit at a time. Finally, the distinction between soft and rigid conditions makes it possible to specify conflicting functional requirements.

Future research will consider the following directions: (1) to enhance the
verification capability by an extension of the proposed framework which can be
facilitated using a principled knowledge representation language (e.g., conceptual
graphs^{29}); and (2) to perform a trade-offs analysis for informal requirements.

This research is partially supported by National Science Council (Taiwan, R.O.C.) under Grant NSC 86-2213-E-008-006. The author would like to thank Professor John Yen for his invaluable comments on an early draft of this article.

**IX.** **APPENDIX: PROOFS**

THEOREM*1. Let E and E**T**be two TSEs over T , and T be a task in T . If E does*
*not contain any invocation of T inG(E**T**), then E* %*T**E**T**5 E ~ E**T*.

*Proof. Since* *G(E) does not contain any task invocation of T in G(E**T*), it
follows from Definition 6 that

*G(E %**T**E**T*)*5 G(E) < G(E**T*) (6)
From Definition 4, we have

*G(E ~ E**T*)*5 G(E) < G(E**T*) (7)
Combining Eqs. (6) and (7), we get*G(E %**T**E**T*)*5 G(E ~ E**T*). Therefore, it is
proved that

*E* %*T**E**T**5 E ~ E**T*. j

THEOREM*2. Let E*1*, E*2*, and E**T**be three TSEs over T . E**T**denotes a TSE in which*
*T appears. (E*1*~ E*2)%*T**E**T**5 (E*1%*T**E**T*)*~ (E*2%*T**E**T*).

*Proof. The theorem can be trivially proved based on the Definintion 6 and*
Definition 4. Based on Definition 6, we have

*G((E*1%*T**E*2))5;*s*_{1}[G(

## <

*E*

_{1}),;

*s*

_{2}[G(

*E*

_{2})

*(s*1%*t**s*2)

From Definition 4, we know that*G(E*1*~ E*2)*5 G(E*1)*< G(E*2). Therefore,
*G(E*1*~ E*2)%*T**E**T*)*5 G(E*1%*T**E**T*)*> G(E*2%*T**E**T*) j
THEOREM *3. Let E*1 *and E*2 *be two TSEs over T , E*1 *5 (a, T, b(c*1, c2*)), and*
*E*2*5 (T, b(c*1;*g)), where a, c*1,c2*andg are TSEs, and b is a condition. E*1%*T*

*E*2*5 (a, T, b(c*1,c2;g)).

*Proof. From Definition 4, we know that*
*G(a, T, b(c*1,c2))

*5 hs9*1*n t n b? n s9*2*n s9*3*us9*1[ G(a) ` t is an invocation of T ` b? is a
task for testing*b ` s9*2[ G(c1)*` s9*3[ G(c2)j

*< hs*1n t n¬b? n hus91[ G(a) ` t is an invocation of T ` b? is a
task for testingb ` h an empty task sequencej

*G(T, b(c*1;g))

*5 ht n b? n s9*2*n s9*4*n s9*5*u t is an invocation of T ` b? is a*
*task for testingb ` s9*2[ G(c1)*` s9*4*[ S ` s9*5[ G(g)j

*< ht n*¬b? n hu t is an invocation of T `¬b? is a task for
*testing*¬b ` h is an empty task sequencej

and that (1) for any sequence*kt n b? n s9*2*n s*4*n s9*5*l [ G(T, b(c*1;g)), we know that
there always exists a sequence *kt n b? n s9*2*n s9*3*l such that kt n b? n s9*2*n s9*3l is a
subsequence of*kt n b? n s9*2*n s9*4*l (i.e., kt n b? n s9*2*n s9*4*l 5 kt n b? n s9*2*n s9*3*n s0*4l, where
*s*04 *[ S ), and (2) for any sequence kt n*¬b? n hl [ G(T, b(c1;g)), it is obvious
that*kt n*¬b? n hl is a subsequence of ks91*n t n*¬b? n hl [ G(a, T, b(c1,c2)).

Based on Definition 6, the result of composition is
*G(E*1%*T**E*2)

*5 hs9*1*n t n b? n s9*2*n s9*3*n s0*4*n s9*5*us9*1*[ G(a) ` t is an invocation of T ` b? is a*
*testing task forb ` s9*2[ G(c1)*` s9*3[ G(c2)*` s0*4*[ S ` s*5[ G(g)j

*< hs9*1*n t n*¬b? n hus91*[ G(a) ` t is an invocation of T `*¬b? is a
*task for testingb ` h is an empty task sequencej*

Based on Definition 4, we have
*G(a, T, b(c*1,c2;g))

*5 hs9*1*n t n b? n s9*3*n s0*4n s95*us9*1*[ G(a) ` t is an invocation of T ` b? is a*
*testing task forb ` s9*2[ G(c1)*` s9*3[ G(c2)*` s0*4*[ S ` s9*5[ G(g)j

*< hs9*1*n t n*¬b? n hus91*[ G(a) s t is an invocation of T `*¬b? is a
*task for testingb ` h is an empty task sequencej*

*Hence, the theorem (E*1%*T**E*2)*5 (a, T, b(c*1,c2;g)) is proved. j
THEOREM*4. Suppose the initial state description*w*to a TSE E is in a disjunctive*
normal form:w5 (w1~w2~ . . .w w*n**), where*w*i**in*w*is a conjunction of literals.*

*If E* *5 («, T) and ;i*w*i* *R B**T**, then (*w1 ~ . . . ~w*n**)/E* 5 w1*/T*~ . . . ~
w*n**/T.*

*Proof. The proof of this theorem is outlined below: Since b*u5w1 ~ . . . ~w*n*

⇔*b*u5w1*~ . . . ~ b u5*w*n**, we can derive that a*u5 (w1~ . . . ~w*n**)/T*⇔*a*u5
w1*/T*~ . . . ~w*n**/T. Given the precondition of the task can be deduced from*
everyw*i*, we know that everyw*/T is valid. Thus, the theorem is proved.* j
THEOREM *5. Suppose the initial state description*w *to a TSE E is a disjunctive*
*normal form:*w5 (w1~w2~ . . . ~w*n**), where*w*i**in*w*is a conjunction of literals.*

*E* *5 (T*1*~ T*2)

*If* w 5 w9 ~ w*0 where*w*9 and* w*0 are in disjunctive normal form, such that*

;w*i**in*w*9,*w*i**R B**T*_{1}*, and*;w*j**in*w*0,*w*j**R B**T*_{2}*, then (*w9 ~w*0)/E 5*w*9/T*1~ (w*0)/T*2.
*Proof. This theorem can be trivially proved by showing that since* w0 can not
deduce the precondition of T,w*0/T*1is not defined. Similarly,w*9/T*2is not defined

either. j

THEOREM*6. (Inconsistent Refinement). LetkC**T**, E**T**l be a task specification of T,*
*andkT, g, S T, E**M**l a method specification M of T. M is an inconsistent refinement*
*of T, one of the following holds:*

*1. B**T*s*y B**M*.
*2. P**T*s*y P**M*.
*3. R**T*s*y R**M*.

*4. R**T**` S**T*s*y R**M**` S**M*.

*Proof. This theorem can be trivially proved by following directly from Definition*

12 and 13. j