Received 5 November 2015; accepted 15 March 2016; published 18 March 2016

ABSTRACT

In this paper, we focus on investigation of the predicate transformer semantics of the contract language introduced by Back and von Wright in their book titled as “Refinement Calculus: A Systematic Introduction” (Springer-Verlag, New York, 1998) in the framework of fuzziness. In order to define fuzzy operations, i.e., fuzzy logic connectives, we take into account implicator ® and its associated T-norm Ä based on residuated lattice theory. Based on these basic fuzzy operations, we introduce the angelic and demonic updates of fuzzy relations. They are the basis of fuzzy predicate transformers in the sense of that any strongly monotone fuzzy predicate transformer can be represented as the sequential composition of the angelic and demonic updates. Together with the standard strong negation, we set up the duality between the angel and demon. The fuzzy predicate transformers semantics of contract statements is established and a simple example of contract statements is given.

Keywords:

Contract Language, Formal Semantics, Residuated Lattice, Fuzzy Predicate Transformers

1. Introduction

There are four main approaches to describe the semantics of some language, i.e., the denotational [1] , the opera- tional [2] , the axiomatic [3] and the algebraic [4] approaches. Predicate transformers semantics [5] [6] is a kind of axiomatic approach to describe semantics of languages. Each statement in a language is characterized by the way it transforms postconditions to preconditions.

Back and von Wright in [7] introduce a contract language ( a detailed introduction in Section 2) describing games that are played between two opponents, called the angel and the demon. The syntax of a contract state- ment S is given by (in BNF-form)

Here P is a relation term and I is a set of higher-order logic which is simply thought of as an index set.

Back and von Wright investigate the transformer semantics of contract language in the Boolean case that the relation P is a classical relation P from X to Y. The angelic update in an initial state x establishes the

postcondition if there is at least one final state y with satisfying q. The state y satisfying q means or. Therefore,

.

Similarly, the demonic update in an initial state x establishes postcondition q if all final state y with satisfy q, described by

.

For a given postcondition q, both angelic and demonic updates define preconditions over initial states, describing if initial states satisfy those updates (preconditions), then their outputs of program at these initial states will satisfy the postcondition q. Therefore, both updates define predicate transformers.

Ying in [8] investigates the probabilistic case of Back-Wright contract language. He generalizes the boolean relation to the probabilistic one. Ying sets up the probabilistic semantics of the contract statements based on the probabilistic logic through probabilistic predicate transformers [6] [9] . The probabilistic model for the guarded language is also studied in [10] .

This paper focuses on the establishment of fuzzy semantics of contract language based on fuzzy predicate transformers [11] . Here, the relation P is a fuzzy relation [12] from initial states to final states. For initial state x and final state y, the value, the membership degree of state belonging to the fuzzy set P, describes indeed the possibility degree of the y to be the output of this program that fuzzy relation P defines from the x. Our goal is twofold: (1) We set up the fuzzy predicate transformer semantics of contract statement S,

which maps a postcondition a over final states, i.e., a fuzzy predicate, into a precondition, a fuzzy predicate over initial states. For a given initial state x, the value is the possibility degree of that

contract statement S establishes the postcondition a from the x. (2) We study the basis of contract languages such as the duality between angel and demon and the Normal Form Theorem that describes which contract statements are represented as the composition of the angelic and demonic updates.

In our investigation, the residuated lattice theory, which plays an extremely important role in modern fuzzy logic theory, is a foundation [13] . In a residuated lattice, are used to model the fuzzy connectives: disjunction, conjunction, production and implication, respectively, as well as strong negation to model fuzzy not.

The organization is as follows. In Section 2, we introduce the contract language in detail. We give an example to explain the contract language and explain why we need to deal with contract language in the framework of fuzziness. In Section 3, we recall some basic notions of residuated lattice. In Section 4, we recall the notion of fuzzy relations and introduce ones of fuzzy predicates and fuzzy predicate transformers. A decomposition of fuzzy predicate is given. In Section 5, we introduce two kinds of basic predicate transformers through updates: the angelic and demonic updates. The angelic update is defined via Ä and the demonic update is defined via ®. Moreover, we analysis why it is better to use Wang’s adjoint pair in defining the angelic and demonic update. In Section 6, we set up the fuzzy semantics of contract statements based on the fuzzy predicate transformers. An example is also given in this section. In Section 7, we introduce the duality and give the Duality Theorem which shows the duality between the angel and demon. In Section 8, we consider the monotonicity of fuzzy predicate transformers. We introduce the notion of strongly monotone fuzzy predicate transformers, and prove the Normal Form Theorem which shows that strongly monotone fuzzy predicate transformers can be represented as the sequential composition of the angelic and demonic updates. The followed is the section of conclusion and future work.

2. Contract Language

Back and von Wright introduce a contract language describing games that are played between two opponents, called the angel and the demon, in their book titled as “Refinement Calculus: A Systematic Introduction” (Springer-Verlag, New York, 1998) [7] . The syntax of a contract statement S is given by (in BNF-form)

Here P is a relation term and I a set of higher-order logic which is simply thought of as an index set. We assume that there is a rule that associates a contract statement with each index in a meet (and similarly for a join).

We will interpret contract statements in terms of a game that is played between two opponents, called the angel and the demon. The game semantics describes how a contract statement S encodes the rules of a game. For a play (or execution) of the game (statement S, we also give the initial position (initial statement) of the game and a goal (a postcondition) that describes the set of final states that are winning positions.

For a given postcondition q, the angel tries to reach a final state that satisfies q starting from the initial state x. The demon tries to prevent this. Both follow the rules of the game, as described by the statement S. The statement determines the turns of the game, as well as the moves, where each move either leads to a new state or forces the player that is to make the move to quit (and hence lose the game). Each move is carried out by either the angel or the demon.

There are two basic moves, described by the demonic and the angelic update statements. The angelic update statement is executed by the angel in state x by choosing some state y such that holds, i.e.,. If no such state exists, then the angel can not carry out this move and quits (loses). The demonic

update statement is similar, except that it is carried by the demon. It chooses some state y such that holds. If no such state exists, then the demon can not carry out the move and quits.

The sequential composition is executed in initial state x by the first playing the game in initial state x. If this game leads to a final state y, then the game is played from this state. The final state of this game is the final state of the whole game.

The demonic is executed in initial state x by the demon choosing some game, to be played in initial state x. If, then there is no game that can be played in initial state x, and the demon has to quit. The angelic choice is executed similarly, but by the angel.

In the remaining of this section, we will give an example describing contract language and explain why we need to deal with contract language in the framework of fuzziness.

An example in [7] , two opponents are components of a computer system, one could be a client, and the other could be server. The client issues requests to the server, who carries out the requests according to the specification that has been given for the possible requests. The server procedures that are invoked by the client’s requests have conditions associated with them that restrict the input parameters and the global system state. These conditions are assertions for the client, who has to satisfy them when calling a server procedure. The same conditions are assumptions for the server, who may assume that they hold when starting to comply with a request. The server has to achieve some final state (possibly returning some output values) when the assum- ptions are satisfied. This constitutes the contract between the client and the server.

There is an interesting form of duality between the client and the server. When we are programming the client, then any internal choices that the server can make increase our uncertainty about what can happen when a request is invoked. To achieve some desired effect, we have to guard ourselves against any possible choice that the server can make. Thus, the client is the angel and the server is the demon. On the other hand, when we are programming the server, then any choices that the client makes, e.g., in choosing values for the input parameters, increases our uncertainty about the initial state in which the request is made, and all possibilities need to considered when complying with the request. Now, the server is the angel and the client is the demon.

In order to formalize this contract, R.-J. Back and J. von Wright introduce the notion of angelic and demonic update. Let P be a relation from X to Y, a predicate and. Then the angelic and demonic update are defined respectively,

and

Example. Let be the set of clients and the set of servers. The relation P is defined as follows:

Assume P is given in Table 1.

Let q is a predicate which means the servers that can be free to download the film “Gone with the wind”. We assume. In fact, p can be seen as a Boolean predicate

In the sense of this, we call the set to predicate. It is easy to get and. Hence and transform the postcondition (goal) p to some precondition, i.e., they are predicate transformers. means that the client connects some server y and can be free to download

the film “Gone with the wind” from y by adopting angelic approach. At this time, we call the initial state can establish the postcondition p by the angelic approach. Thus, initial state can not establish the postcondition p by the demonic approach.

We can see that the underlying logic of this example is two-valued since starting from an initial state, the game reaches a final state or not and final state satisfies given condition (predicate) or not.

However, we can usually say how many possibilities a client connects a server since the tolerated connection time which is caused by the network; how many possibilities the servers can be free to download the film “Gone with the wind” since the properties of servers; thus how many possibilities a client can establish the postcondition(i.e. how many possibilities this client can be free to download this film). That is, it is reasonable to generalize the classical relation into fuzzy relation and the classical predicate into fuzzy predicate. Thus, we generalize the underlying two-valued logic of contract language into fuzzy logic.

3. Residuated Lattice Theory

We note, in the classical two-valued logic, and ® in the angelic and demonic update of Back and von Wright, are an adjoint pair. This also motivates us to consider the angelic and demonic update in the framework of residuated lattice. Residuated lattices, introduced by Dilworth and Ward in [13] , are a common structure among algebras associated with logical systems. As an important and ideal structure, residuated lattices play an extremely important role in modern fuzzy logic theory.

Definition 3.1 [14] A residuated lattice on L is an algebra

with four binary operations and two constants such that

• is a lattice with the largest element and the least element w.r.t. the lattice ordering,

• is a commutative semigroup with the unit element, i.e. Ä is commutative, associative, and for all,

• Ä and ® form an adjoint pair, i.e.

Given a residuated lattice, let us define a unary operator, referred to as the precomplement operator, by [15] .

In what follows, Ä is sometimes called generalized triangular norm (some literature also call it product) and ® is called the residuum of Ä. We denote by, an implicator I is called left monotonic (resp. right monotonic) iff for every, is decreasing (resp. is increasing). If I is both left monotonic and right monotonic, then it is called hybrid monotonic [15] . Clearly, when implicator I is hybrid monotonic, the corresponding adjoint Ä is monotonic, i.e., if, at this time, Ä is called triangular norm.

Definition 3.2 [15] Let be a residuated lattice, be defined as above. If holds for all, then is called a regular residuated lattice.

Example. Taking, for any, the implication operator ® and the generalized triangular norm Ä are defined as follows:

• Łukasiewicz’s adjoint pair:

• Gödel’s adjoint pair:

• Goguen’s adjoint pair:

• Wang’s adjoint pair:

For the above four situations, one can verify that are residuated lattices. However, residuated lattices based on Gödel and Goguen implication operators and the corresponding adjoint are not regular since for any, the others are regular.

Remark. Ying in [8] investigates the probabilistic game semantics of contracts in Section 8. He uses the probabilistic logic based on Goguen implicator and the corresponding adjoint. Hence, Ying can not get the duality theorem in Section 8( Theorem 8.4).

The following properties are useful for our discussion. Their proofs are straightforward and can be found in, e.g., [16] [17] .

Proposition 3.3 Let be a regular residuated lattice. Then for any,

(1) if and only if

(2);

(3)

(4) and

(5)

(6)

(7) and;

(8)

(9) ,

Note that, in this paper, we use a regular residuated lattice with the hybrid monotonic implicator.

4. Fuzzy Relation and Predicate Transformers

This section will recall three basic notions of fuzzy predicates, fuzzy relations and fuzzy predicate transformers, on which we define some operations.

4.1. Fuzzy Predicates

This paper focuses on the establishment of fuzzy semantics of contract statements based on the fuzzy predicate transformers. Now we will recall these notions of fuzzy predicate and fuzzy predicate transformers.

Definition 4.1 A fuzzy predicate on a state space X is any mapping from X to the unit interval [0,1]. We denote the set of fuzzy predicates on X by. The partial order on is defined pointwise: For,

.

Remark. Indeed, fuzzy predicate on X in this paper is in fact fuzzy set on X, we call it fuzzy predicate in order to coincide with the notion in the computer science. On the other hand, usually the notion fuzzy predicate is different from that of fuzzy set. For example, in [11] [18] fuzzy predicate over a dcpo X, a directed complete poset, is Scott continuous function from this dcpo to the unit interval where Scott-continuous function f refers that f preserves the order (i.e.,) and suprema of directed sets (i.e., for every directed family in X) (see, Definition 3.1, [18] ). When we only consider discrete state spaces X (i.e., a dcpo such that if and only if for all), fuzzy predicate is just fuzzy set.

The join and meet of a family of fuzzy predicates are given by

The fuzzy predicate space is a completely distributive lattice. The bottom element is false, where and its top element is true, where for any.

For any, we define the constant fuzzy predicate as the constant function from X to [0,1], i.e., , for all For any, we define a point fuzzy predicate as if and 0 otherwise.

In addition to the greatest lower bound and the least upper bound, we introduce the logical connectives: negation, the product Ä and the corresponding adjoint ® on fuzzy predicates pointwise as follows:

For all and

In particular, , where

It is easily verified that is a regular residuated lattice.

Proposition 4.2 (Decomposition of fuzzy predicates) For any, we have

and

where is an adjoint pair.

Proof. We have by the definition of residuated lattice for every.

Since, we have that which proves the second equality. □

4.2. Fuzzy Predicates Transformers

The notion of fuzzy predicate transformers comes from [18] , the authors use it to set up the logical semantics of possibility computation.

Definition 4.3 (1) A fuzzy predicate transformer (FPT, for short) from the state space X to Y is any mapping from to, denoted by.

(2) The refinement order between fuzzy predicate transformers is pointwise defined, i.e., for two fuzzy predicate transformers t and, if and only if for any fuzzy predicate

(3) A fuzzy predicate transformer is monotonic if for any, implies that holds.

For any, we define a constant FPT by setting for any fuzzy predicate. And we denote the identity FPT by skip over state space X, defined as for any fuzzy predicate.

All operations on fuzzy predicates may be pointwise extended to fuzzy predicate transformers:

in particular,

for all,.

Moreover, we define the sequential composition of fuzzy predicate transformers. For and the sequential composition of t and is defined by for all.

4.3. Fuzzy Relations

Relations appear in many fields of mathematics and computer science. In classical mathematics these relations are usually crisp, i.e., two objects are related or they are not. However, many relations in real-word applications are intrinsically fuzzy, i.e., objects can be related to each other to a certain degree [19] .

Definition 4.4 For given two state spaces X and Y, a fuzzy relation P from X to Y is a fuzzy set on the product. We write for the space of fuzzy relations from X to Y. The order between fuzzy relations is defined as if and only if for all for given two fuzzy relations P and Q.

The join and meet of a family of fuzzy relations on are given by

For the algebraic structure of, we have that is a completely distributive lattice. Its bottom (the empty relation), denoted by False, and top (the complete relation), denoted by True are defined by

for and. The identity function over the state space X is represented by the relation defined as if and 0 otherwise. We often omit the subscript X.

Definition 4.5 [12] [20] For fuzzy relations and, composition where T is a triangular norm: is defined by

for all and.

Some basic properties of composition are collected in the next proposition. We omit the straightforward proofs.

Proposition 4.6 Let and Then

(1);

(2);

(3); and

(4). ,

Remark 2. holds, but does not hold in general. The following is an example.

Let for all and and for all and. And let Ä be the corresponding adjoint of implicator of Wang’s. Then

However,

This shows that does not hold.

Further, the following proposition is easily gotten.

Proposition 4.7 Let, and, then. ,

5. Basic Predicate Transformers

This section will introduce two basic fuzzy predicate transformers through an update method applied to fuzzy relations and analysis them through adjoint pairs.

5.1. Angelic and Demonic Update

As documented in [7] , for a given Boolean relation P from X to Y and a Boolean predicate. The angelic update and the demonic update are formally defined as follows:

Ying in [8] defines the notions of angelic and demonic updates in the probabilistic case by translating the two logical formulae above into probabilistic logic (see Definition 6, page 334).

Here, we define these updates in the possibility case. Since the existential and universal quantifiers can be interpreted by supremum and infimum, respectively, one arrives at the following definition.

Definition 5.1 Let X and Y be two state spaces and. For all and, the angelic update and the demonic update are respectively defined by

where is an adjoint pair.

Both angelic and demonic updates define fuzzy predicate transformers from state space X to state space Y. That is, for any fuzzy predicate (postcondition), we get a fuzzy predicate (precondition) (resp.). We call in initial state x, the angelic update establishes the postcondition a

with the degree if the state x satisfies fuzzy predicate with the degree, which is just meaning of membership degree of the state x belonging to fuzzy set.

Remark. The angelic and demonic updates are similar to the definition of upper and lower fuzzy rough approximation in [19] , but a little difference.

where A is a fuzzy set in X. We can see that if P is fuzzy relation in, then and are functions from to. However, and are functions from to.

In next section, we will establish the fuzzy predicate transformer semantics of contract statements. Here, we discuss some properties of these basic updates.

Proposition 5.2. □

Proposition 5.3 Let. Then

if and only if if and only if. □

Proof. We only prove implies. Let. Then for any and,. That is,

In particular, we take, then we have. By the arbitrariness of, we get. □

This proposition tells us that the order is preserved by the angelic update and reversed by the demonic update.

The following two propositions present homomorphic properties of the angelic and demonic update operators on fuzzy relations.

Proposition 5.4 Let be three state spaces, and. Then

(1)

(2).

Proof. We only prove (2), the proof of (1) being similar. For and, we have:

□

The above proposition shows that the updates and the composition of fuzzy relations commute, whereas the next proposition indicates that the angelic update preserves unions of fuzzy relations, and the demonic update changes a union of fuzzy relations into a meet.

Proposition 5.5 Let be state spaces and. Then

(1);

(2).

Proof. The straightforward proofs use Definition 5.1 and properties of Ä and ®. □

5.2. Analysis

In this subsection, we will analysis angelic and demonic update through different adjoint pairs. We wish to choose more appropriate those to apply contract language.

Usually, in some game, we always assume “I” am angel and opponent is demon. I always wants to win and prevents opponent to win. For fuzzy situation, I always tries to maximize the possibility of wining and minimize possibility of winning of the opponent. Since, in this paper, we discuss contract language only under regular residuated lattice, we compare Łukasiewicz’s adjoint pair with Wang’s adjoint pair for the sake of familiarity.

For a given postcondition and a state, the angelic update in state x establishes the postcondition a with the degree of. By the definitions of Ä in Łukasiewicz’s adjoint pair and Wang’s adjoint pair, this degree is equal to

and

respectively.

It is easy to verify that for any,. Hence, , where and refer to, in the definition of angelic update, the product Ä taken is in Wang’s adjoint pair and Łukasiewicz’s adjoint pair, respectively. That is, for me, the possibility of winning (i.e. satisfying a) when using Ä in Wang’s adjoint pair is greater than or equal to that when using Ä in Łukasiewicz’s adjoint pair for initial state x.

On the other hand, the demonic update in state x establishes the postcondition a with degree of. By the definitions of ® in Łukasiewicz’s adjoint pair and Wang’s adjoint pair, this degree is equal to

and

respectively.

Clearly, for any,. Hence, , where and refer to, in the definition of demonic update, the implicator ® taken is in Wang’s adjoint pair and Łukasiewicz’s adjoint pair, respectively. That is, for opponent, the possibility of winning (i.e. satisfying a) when using ® in Wang’s adjoint pair is smaller than or equal to that when using ® in Łukasiewicz’s adjoint pair for initial state x.

Hence, considering the previous two factors, it seems more appropriate to use Wang’s adjoint pair in contract language.

6. Fuzzy Semantics of Contract Language

Based on the previous discussion, we propose the fuzzy predicate transformer semantics of the contract language. The syntax of contract statements is given by

Here P is a fuzzy relation term and I a set of higher-order logic which is simply thought of as an index set.

Definition 6.1 The fuzzy predicate transformer semantics of a contract statement S from X to Y is defined to be a fuzzy predicate transformer which is inductively defined as follows:

We are supposed to give a contract statement S which is described by a fuzzy relation P from state space X to state space Y. These semantics of the angelic update and the demonic update are respectively defined as the angelic update and the demonic update. Both map postconditions to preconditions.

Now, we continue the example in section three. Fuzzy relations from X to Y are given in Table 2.

A postcondition a means the possibilities that the servers can be free to download the film “Gone with the wind”, which can be given as a fuzzy predicate as follows.

means the possibility 0.2 that the server can be free to download the film `Gone with the wind’.

If we take ® and Ä in the demonic and angelic update to Wang implicator and its adjoint, then through computing, we can get

and

and

We can see are all fuzzy predicates on the clients set X, which means the possibilities that the clients download the film `Gone with the wind’ by the angelic and demonic approach, respectively. For example, means the possibility 0.8 that the client downloads the film “Gone with the wind” by the angelic approach.

Suppose the contract statement. This statement describes these rules: firstly taking the demon to R1 and then taking the angel to R2 or the demon to R1. Now we get that

If we have the contract statement, then

From these two formulae above, we can get that the contract statement S1 will establish the postcondition a (i.e. downloads the film “Gone with the wind”) from the initial state with the possibility degree of 0.75 However, S2 has this degree of 0.83.

7. The Duality

The angelic and demonic updates are basic strategies of contract language. The angel always wants to win, however, the demon always tries to prevent this winning. Of course, the angel also prevents the demon to win. Therefore, the angel and demon are a pair of opponents which present a duality between them.

In this section we introduce a duality for fuzzy predicate transformers through negation to confirm this duality. The specification language of Back and von Wright [21] was based on the fundamental dualities between demonic and angelic nondeterminism and between nontermination and miracles. Dijkstra and Scholten [5] introduced a notion of converse predicates that is closely related to duals.

Definition 7.1 The dual of a fuzzy predicate transformer is defined by, where.

As, it follows that and that implies If t is monotone, then so is.

Definition 7.2 Let. Then

(1) t has the scaling property, if for all and.

(2) t has the implication property, if for all and.

The following proposition shows that the scaling property and the implication property are dual in the sense that an FPT t has the scaling property if and only if has the implication property.

Proposition 7.3 Let t be an FPT from X to Y. Then, t has the scaling property if and only if its dual has the implication property, where is an adjoint pair.

Proof. Assume that t has the scaling property, i.e., for any and Then,

So, the dual has the implication property.

Conversely, let t have the implication property. Then

Therefore, has the scaling property. □

Theorem 7.4 (Duality Theorem) The following dualities hold for fuzzy predicate transformers:

Proof. We only prove and. Let. For any and,

Hence.

Now, let, and Then,

,

Proposition 7.5 Let, then has the scaling property and has the implication property.

Proof. Due to the duality, we only need to prove that has the scaling property. Let and. Then:

,

8. Monotonicity

In the previous section, we set up the fuzzy predicate transformer semantics of contract statements. It is well- known that not all predicate transformers are interpretations of programming statements. Dijkstra [22] stated that predicate transformers accepted as semantic functions of programming statements are required to satisfy certain healthiness conditions. The basic conditions, that he imposed originally, were strictness, monotonicity, conjunc- tivity and disjunctivity. With respect to possibility computations, we proposed healthiness conditions in [18] (Definition 3.4, p. 2666).

R. J. Back and J. von Wright in [7] discovered a very interesting theorem, called the Normal Form Theorem, which says that all monotone predicate transformers can be represented in terms of angelic and demonic updates. In this section, we will introduce the notion of strong monotonicity and establish the Normal Form Theorem for fuzzy predicate transformers. which answers what fuzzy predicate transformers can be represented by angelic and demonic updates of fuzzy relations (see, Theorem 8.6 below).

Definition 8.1 [23] Let X be a state space. For two fuzzy predicates a and b in X, the degree of I-inclusion of a in b is given by

Note that this notion is also called strength of implication by Ying in [8] .

For instance, let X be the set of non-negative integers and let, for all, and for all. Then, both a and b are fuzzy predicates on X. We first notice that

for although holds for all. But, it is reasonable to say that a implies b with a very high degree very close to 1.

Definition 8.2 Let X and Y be two state spaces, and. Then t is said to be strongly monotone if and only if for all, we have.

It is easy to see that strong monotonicity implies (weak) monotonicity, but the converse does not hold.

Proposition 8.3 If FPT t is strongly monotone then so is.

Proof. Assume that t is a strongly monotone FPT from X to Y. We need to show that the dual FPT is strongly monotone, too. Now, , due to the strong monotonicity of t, we have and

Therefore, is a strongly monotone FPT. □

We will show that strong monotonicity can be derived from (weak) monotonicity and the scaling property.

Proposition 8.4 Assume that an FPT is monotone. Then, if t has the scaling property or the implication property, then t is strongly monotone.

Proof. We have to show:. For this, it suffices to show: whenever, then We need to verify it for the case of t being the scaling property. For another case, We can also verify it using the adjoint between Ä and ® in the following induction. But, we like to get this verification by using the duality between scaling and implication (Proposition 7.3 and 8.3).

,

We now establish the normal form theorem for fuzzy predicate transformers. We first give a theorem which says that updates of all basic statements are strongly monotone and that operations for constructing compound statements also preserve strong monotonicity.

Theorem 8.5 Strong monotonicity is closed under composition, meet, and join of fuzzy predicate transformers.

Proof. (1) We prove that meet of fuzzy predicate transformers preserves strong monotonicity. Let and. Then

Hence, meets preserve strong monotonicity. Similarly, we can prove that joins of fuzzy predicate transformers preserve strong monotonicity.

(2) We prove that composition preserves strong monotonicity. Let, and. Then

Hence, composition preserves strong monotonicity. □

Now we present the Normal Form Theorem for strongly monotone fuzzy predicate transformers.

Theorem 8.6 (Normal Form Theorem) Let X and Y be two state spaces and. Then t is strongly monotone if and only if, for some fuzzy relations P and Q.

Proof. The “if” part. By Proposition 7.5, has the scaling property and the implication property. As and are monotone, Proposition 8.4 implies that and are strongly monotone.

The “only if” part. We define fuzzy relations and as follows:

for all and. Then we have

On the other hand, for any, since t is strongly monotone,

Therefore,

We have gotten that. Hence. □

9. Conclusion and Further Work

We have given the fuzzy predicate transformer semantics of contract langauge introduced by Back and von Wright in [7] . Adjoint pair of a residuated lattice is used to define the fuzzy logic connectives: implication and production. In terms of these fuzzy operations, we have defined the fuzzy updates of the angelic and demonic statements in contract language. These two updates are the basis of fuzzy predicate transformers in the sense that strongly monotone fuzzy predicate transformers are just the sequential composition of these angelic and demonic updates of two fuzzy relations, which is called as Normal Form Theorem. Together with the standard strong negation, we have set up the duality of fuzzy predicate transformers. The duality describes the duality between the angel and the demon, which says that the angel and demon in games can change their strategies each other. In the future, we need to consider the denotational [1] and operational semantics [2] in the frame- work of fuzziness. Moreover, those semantics of contract language should be considered by taking into count the conditional structure if b then S₁ else S₂ and loop structure while b do S.

Recently, Wang and Zhou [24] establish the foundation of quantitative logic. Pei [25] investigates the full implication of fuzzy reasoning. Both will promote the research on the quantitative semantics with respect to fuzzy programming language.

Acknowledgements

The first author was supported by the Zhejiang Provincial Natural Science Foundation of China (LY13F020046) and Zhejiang Provincial Education Department Fund of China (Y201223001). The second author acknowledges support from the Natural Science Foundation of China (No. 61370100) and the Shanghai Leading Academic Discipline Project (B412).

Cite this paper

HengyangWu,YixiangChen, (2016) Fuzzy Semantics of Contract Language. Applied Mathematics,07,422-439. doi: 10.4236/am.2016.75039

References

NOTES

^*Corresponding author.