文档库 最新最全的文档下载
当前位置:文档库 › To appear in Automated Software Engineering Behavioural Conflicts in a Causal Specification

To appear in Automated Software Engineering Behavioural Conflicts in a Causal Specification

To appear in Automated Software Engineering Behavioural Conflicts in a Causal Specification
To appear in Automated Software Engineering Behavioural Conflicts in a Causal Specification

To appear in Automated Software Engineering

3 August 1999

Behavioural Conflicts in a Causal Specification

Jonathan Moffett

Department of Computer Science, University of York

Heslington, York YO1 5DD, UK

jdm@https://www.wendangku.net/doc/4f5895464.html,

Andrew Vickers

Praxis Critical Systems

20 Manvers Street, Bath BA1 1PX

ajv@https://www.wendangku.net/doc/4f5895464.html,

Abstract

Inconsistencies may arise in the course of specification of systems, and it is now recognised that they cannot be forbidden. Recent work has concentrated on enabling requirements descriptions to tolerate inconsistency and on proposing notations that permit inconsistency in specifications. We approach the subject by examining the use of an existing causal language, which is used as a means of specifying the behaviour of systems, to specify, identify and resolve behavioural inconsistencies. This paper is an exploration of the kinds of inconsistency that can arise in a causal specification, how they can be discovered and how they can be resolved. We distinguish between inconsistencies in the structure of a specification, which are assumed to have been removed previously, and inconsistencies in behaviour which, being dynamic in nature, we describe as conflicts.

Our approach concentrates on the identification of conflicts in the specified behaviour of a system. After summarising the causal language, we describe a classification of behavioural conflicts and how they can be identified. We discuss possible methods of resolution, and propose a simple process to aid the identification and resolution of conflicts. A case study using the causal language illustrates our approach.

1. Introduction

1.1 Background and Aims

It has long been recognised that inconsistencies may arise in the course of specification of systems and that the goal of a single unified view of a system is difficult to achieve. The traditional view was that inconsistencies must either be forbidden, or removed at as early a stage as possible.

However, it became recognised that the various stakeholders in a system might have different, and possibly inconsistent, viewpoints [1], and that requirements descriptions must tolerate, and even embrace, inconsistency. Gabbay [2] proposed that inconsistency should be made

respectable. Subsequently his work has been built on by Nuseibeh and others [3, 4], and they have proposed notations that permit inconsistency in specifications.

We approach the subject from a different direction. An earlier paper [5] proposed the use of a causal language as a means of specifying the behaviour of systems. We pointed out that one of the natural means by which the customers of complex systems express themselves is in terms of causation. We proposed a causal language with two important characteristics:

?It should enable users to specify behaviour using a simple causal notation. Our long-term aim is to integrate causal statements into a specification style based on a restricted natural language;

?The notation should be sufficiently precise to be interpreted in terms of any of several temporal logics, and would therefore be amenable to formal reasoning.

One characteristic of this notation is that it is possible for a causal specification to contain mutually inconsistent causal statements. This paper is an exploration of the kinds of inconsistency that can arise in a causal specification, how they can be discovered and how they can be resolved.

1.2 The Principle of Causality

In order to identify behavioural conflicts we need a unifying principle, and we use the principle of causality – nothing happens without a cause1. If things "behave" only if they are caused then by describing all the behaviour of a system in terms of causal statements we can capture the entire behaviour of a system using a single notation, thus easing the task of analysis. It should be recognised, of course, that there is a cost to be paid by eliminating all other descriptions of how a system can change, because we may be significantly reducing our expressive power. One of the purposes of this paper is to demonstrate one of the benefits to be put onto the positive side of the balance: a systematic approach to describing and finding behavioural conflicts in a system.

Further leverage can be obtained from the principle of causality: an approach to the resolution of some conflicts. Implied in the principle of "nothing happens without a cause" is a hierarchy of behavioural imperatives, discussed in section 4.3.3, which can be used as guidance on how to resolve conflicts between causal statements.

1.3 What Are Behavioural Conflicts?

There are at least three possible levels of inconsistency in a system:

1.The system description is inconsistent so that it is impossible to describe what happens in

it. Typically this is because the entity model has not been completed successfully. We refer to inconsistencies of this kind as structural inconsistencies. Behavioural conflict 1 It will become apparent below (section2.3) that the principle that we use is actually slightly stronger than this; our notation only recognises causation which has an immediate effect. There can only be a gap between cause and effect if this gap is filled by a chain of intermediate direct causes.

analysis will only be possible for those parts of the system for which there is a structurally complete and consistent entity model2.

2.There is a consistent entity model but the behavioural statements are in conflict. This is

the level, behavioural conflicts, at which we are addressing this paper. Behavioural conflicts at this level have one characteristic in common: the conflicts are such that a working system cannot be constructed because it is at some point in contradiction. For example:

?The same condition is simultaneously caused and prevented;

?The predicates for the state of the system will be in contradiction if the causal statements are obeyed.

We describe and analyse these behavioural conflicts in more detail below in section 4.

3.Conflicts that occur in a working system, which we call operational conflicts, e.g.

deadlock, conflicts with safety and security policies, inefficiencies, incorrect output, and all the other ills that beset working systems. Although some of these may perhaps be usefully addressed using a causal specification, we have not attempted to do so in this paper.

We therefore distinguish between inconsistencies in the structure of a specification, and inconsistencies in behaviour which, being dynamic in nature, we describe as conflicts. Our approach concentrates on the identification of conflicts in the behaviour of a system. Inconsistencies in its structure are assumed to have been removed previously by constructing an entity model; in the example that we use in this paper we use an object model that is adapted from [6], but other approaches could also be appropriate.

The scope of this paper is, therefore, those conflicts in a specification with a consistent object model, which prevent the designer from defining the behaviour of the system without contradiction or ambiguity3.

1.4 Paper Contents

The remainder of this paper is structured as follows. Section 2 gives a summary of our causal notation. Section 3 uses fragments from an example lift system to illustrate our use of the causal notation in practice and provide some material with which to perform our analysis of conflicts in the specification. Section 4 uses material from the example to demonstrate and analyse the classes of conflict that we have encountered, and discusses approaches to their resolution. Section 5 discusses a sample of the related work in this field. Finally section 6 discusses the results of the work and reaches some conclusions.

2. Causal Notation

This causal notation introduces a restricted vocabulary of causal words which are intended to be used with existing formal notations. We are not attempting to introduce a new logic, but a 2 We have not addressed the case where the entity model is incomplete, i.e. underspecified, but not inconsistent.

3 Thomas [7], discussed in section 5 below, points out that while there is non-determinism in a specification, the possibility of undesirable interactions cannot be totally eliminated.

notation with an interpretation in terms of existing well-developed temporal logics. In this paper we use extracts from a formal specification for encoding the specification. The specification language Z [8] is used with explicit time.

This section summarises the formal definition of the causal model that is described in more detail in [5]. In section 2.1, we describe the properties of causation. Section 2.2 describes the building blocks of our approach: Time, Events and Conditions; and section 2.3 defines causal expressions.

2.1 Properties of Causation

The properties of causation are discussed in [9] and [10]. We select here those that are particularly pertinent to this paper:

?Causation is transitive: if a causes b and b causes c then a causes c

?Causal laws may be cyclic: a causes b and b causes c and c causes a. However the condition occurrences which result from those laws are ordered in time and thus cannot be cyclic. This is put into context in section ?.

?We distinguish between sufficient cause and necessary cause

?If a is a sufficient cause for b then the occurrence of a is inevitably followed by the occurrence of b.

?If a is a necessary cause for b then b will not occur unless a does. This has two negations in it: "will not" and "unless".

We find it easiest to think in terms of sufficient cause rather than using the double negations of necessity. Accordingly, we treat sufficient causation as primary, and throughout this paper, unqualified "cause" refers to sufficient cause.

2.2 Time, Events and Conditions

This section describes the building blocks of our approach to causation: Time, Events and Conditions.

2.2.1Time

We assume that the instants of time are taken from a given primitive set, which is a strict total order, ordered on (transitive) precedes. We use the informal concept of granularity of time, recognising that it may be appropriate to work with a finer or coarser granularity of time, even in different parts of the same specification. No attempt has yet been made to include granularity in our formal specification. Work of this kind is reported in [11]. They describe a temporal logic language, with extensions permitting a temporal universe composed of temporal domains of different time granularities.

2.2.2Events

We look at executions of the system in terms of the observations of events, each of a named class, made by a single observer, who only observes one event occurring at a time. An event occurrence is a tuple (event class, time of occurrence).

Event occurrences are unique; each event occurrence occurs only once, although a number of events of the same class can occur ordered in time – the StartOf(red) [traffic light] at 15:05 is

a different event occurrence from, but of the same class as, the StartOf(red) at 15:06. For brevity, and where there is no ambiguity, we say "a occurs at time t" (where a is an event class) to mean "an event occurrence of class a occurs at time t ".

2.2.3Conditions

We base our concept of conditions upon intervals of the time line, where intervals are defined by their start and end-points.

A condition class is the name of a set of intervals, and a condition occurrence is one of those intervals, analogous to an instance of an abstract data class. For simplicity we insist that there is no overlap between the occurrences in a condition class. There are two events associated with each condition: StartOf(condition) and EndOf(condition) with their obvious meanings.

An event can be regarded as an interval with no duration, and so we regard event classes and occurrences as special cases of conditions. Conditions hold during their intervals, and a relation, HoldsAt, between Condition and Time, defines those time points at which a condition holds. A function, abbreviated to "~" in this paper, defines the complementary condition, so that ~c holds at those time points at which c does not hold.

Each condition class defines a set of occurrences with some property in common, e.g. those intervals during which a particular traffic light is red. Each useful condition class is associated with one or more predicates, which express the properties of the system which are true while the condition holds, i.e. during each interval for which there is an occurrence of that condition. These properties are expressed in terms of time-dependent variables

In our specification a time-dependent variable is expressed as a function from time to a value variable: Time →?value

The form of a predicate associated with a condition is:

? t:Time ?condition holds_at t ?variable (t) = value

An example of this is shown in section 3.1.2.

2.3 Causal Relationships and Expressions

Causal relationships are universal relationships between conditions. We refer to them in the example below as causal laws, e.g. "striking a match causes fire ". This law does not refer to any particular occurrence of match-striking or fire. However, we may refer to causal instances, typically in the past tense, e.g. "the striking of a match (in a particular location) at 12:09 a.m. on 14/1/97 caused the fire there at 12.10 a.m.".

A causal expression has the following format:

[While Compound_Condition ]condition1 causal_relation condition2

where we refer to condition1 (the causing condition) as the subject and condition2 (the effected condition) as the object of the causal expression.

The While clause limits the applicability of the causal expression to intervals in which the While compound condition holds, e.g. "While there is sufficient oxygen …"

We define four kinds of causal_relation:

?

directCauses : starts a condition or makes an event occur;?

terminates : ends a condition;?

sustains : prevents a condition from ending;? prevents : prevents a condition from starting or an event from occurring.

We give here the formal definitions of directCauses and its generalisation indirectCauses .The reader is referred to [5] for the similar formal definitions of terminates , sustains and prevents . It should also be noted that, arising from these definitions:

? c directCauses d ? c terminates ~d and c terminates d ? c directCauses ~d ? c sustains d ? c prevents ~d and c prevents d ? c sustains ~d

2.3.1 Direct Cause

We regard direct causation as implying that, unless it already holds, the caused condition starts immediately after the end of the causing condition, where "immediate" is governed by the granularity of time within which the observations are taking place. For example, although there may be a perceptible pause between flicking a switch and the light coming on, we may choose to make observations at a sufficiently coarse granularity of time that we can regard the two conditions as abutting. Formally 4:

c directCauses

d ? EndOf c = StartOf d ∨ EndOf c ∈ IntervalOf d

Situations 1 and 2 in Figure 1 illustrates this relationship; in situation 1 d starts immediately after c ends, and in situation 2 d already holds at the end of c . Situation 3 is inconsistent with c directCauses d because it does not show d starting immediately after the end of c .

Time →

c d

Figure 1 Condition c directCauses condition d

2.3.2 Indirect Cause

We define indirect cause in terms of direct cause. A condition c is said to indirectly cause condition d iff we can find intervening direct causes to make up a causal chain, including the case where the chain has only one link. This is defined recursively:

c indirectCauses

d ?

(c directCauses d) ∨

(? b: Condition ? c indirectCauses b ∧ b directCauses d)

4 Ignoring issues of open and closed intervals discussed in [5].

Indirect cause is thus the transitive closure of the directCauses operator. Figure 2 illustrates the general causal relationship. The transitivity of indirect cause follows from its definition.

Time →

b b b Figure 2 Condition

c indirectCauses condition d

3. Example – Lift System

Before expounding the classes of behavioural conflict, we introduce an example system, which provides the reader with an introduction to the notation and us with material to discuss behavioural conflicts. Our example is a lift system, whose description is derived from a textual description that was designed for the requirements engineering module of a Masters course at the University of York. A set of informal requirements for the elevator control system was defined. To avoid duplication, they are set out in section 3.3, where we describe how each one is met by our design.

A full causal specification 5 was written in the Z language and type-checked. For brevity and readability, in this section we only introduce the signatures of variables, and any predicates which are relevant to conflicts are introduced at the appropriate point in section 4.

3.1 Background and Object Model

It is proposed to install a new passenger lift in a new building. An informal object model of the system has been defined. It is illustrated in Figure 3 and described below.

5 Available as a report from the authors, on request.

Figure 3 Lift System

3.1.1The Lift Shaft and Landings

Lift Shaft and Floors

The lift shaft extends over five floors (0 - 4), each of which has a landing door and a control panel. Each floor has an elevation above some fixed point.

Floor

LandingDoor: Door

FloorControlPanel

Elevation: ?

LiftShaft

Floors: seq Floor

Landing Doors

On the landing of each floor there is a door giving access to the lift shaft. Each door is opened and closed by a motor:

?Four conditions are associated with the door: Open, Closing, Closed, Opening ?Aperture is a measure of how far the door is open. FullyOpen is its value when Open holds.

Door

Open, Closing, Closed, Opening: Condition

Aperture: Time →?

FullyOpen: ?

Control Panel on Landings:

On the landing of each floor, near the lift door, there is a control panel containing Up and Down buttons and lights:

Landing

UpButton, DownButton: Event

UpLightOn, DownLightOn: Condition

UpButton and DownButton are events which signal when they are pressed, and the UpLightOn and DownLightOn are conditions which hold when the lights are on.

3.1.2Lift Car

The passengers are carried in a lift car which is moved by a motorised system. The schema that defines the lift car is given after its components have been defined.

Car Door

There is a door on the car, giving access to the floor landings. It is defined identically to the landing doors.

Control Panel in Car

The car has a control panel in it with:

?Buttons and lights for each floor destinations;

?Emergency stop button;

?Door open button;

?Door close button;

As for the control panels on landings, buttons are defined as events and lights as conditions.

Lift Car Conditions and Predicates

Variables of Elevation, Speed and Acceleration are declared as functions from Time to Number. Constant numbers define the maximum speed and acceleration for comfort and safety

There are the following conditions associated with the lift car:?EmergencyBrakeOn: a condition which holds when the emergency brake is on. The brake brings the car to a halt when operated, with a deceleration which is greater than that defined by MaxAccComfort.

?OccupantSensed: a condition which holds when, and can be queried to determine whether there are currently occupants in the car.

?Stationary, InMotion, SpeedComfort, AccComfort: conditions which hold when their associated predicates are true, e.g. AccComfort only holds when the absolute value of Acceleration is less than a defined maximum value for comfortable acceleration:

? t:Time ? AccComfort HoldsAt t ?

abs (Acceleration(t)) < MaxAccComfort

3.1.3Controller

There is a controller module which contains the logic for controlling the system. The state of requests for a floor is defined in the Crequest schema:

?There are three kinds of request for a particular floor: as a result of the UpButton or DownButton having been pressed at that floor, or the relevant FloorReq button having been pressed from within the car.

?One of the main functions of the controller is to decide to which floor the car should go next. PreferredReq holds for only one floor at a time, and defines the next destination. We do not define the algorithm for this.

Crequest

UpReq, DownReq, FloorReq, PreferredReq: Condition

The LiftController schema includes LiftCar and Liftshaft and it is also aware of the position and movement of the car, and a sequence of Crequest to define the state of requests for each floor: LiftController

LiftShaft

LiftCarDefn

AtFloor: seq Condition

AtAFloor: Condition

MovingToFloor: seq Condition

Requests: seq CRequest

The LiftController schema includes LiftCar and Liftshaft and it is also aware of the position and movement of the car, and a sequence of Crequest to define the state of requests for each floor: 3.2 The Working of the Lift System

We describe here, using extracts from the formal specification, the essentials of the working of the system. This illustrates the application of the causal language and provides the basis for the investigation of conflicts described in section 4.

Calling the Lift

The lift system is a reactive system, and a cycle of activity is started by a passenger pressing a button on a landing, e.g. the Up button. This directly causes the associated light to come on and a request to be registered with the controller. Also it indirectly causes the lift eventually to arrive at the floor:

Whenever there is a change in the status of a request, the next destination floor may change. This is regularly recalculated by the Controller according to its algorithm, which is not visible at this level of description.

Despatching the Lift

The Controller, having calculated the next destination floor, despatches the lift to that floor.

Arriving at a Floor

When the lift arrives at a floor, the door starts to open, and opening is terminated when the door is fully open. The request to go to that floor is then terminated.

While the lift is at a floor, pressing the Up or Down button on the landing or Open button in the car causes the door to open if it is not open already.

We do not model the act of passengers entering and leaving the lift, but if there are any passengers in it the condition OccupantSensed holds.

Request a Destination

When a passenger presses a floor button, the request to go to that floor is registered and the door starts to close. Closing is terminated when the door is Closed. The controller can then service its next call.

3.3 Requirements for Lift System

A number of informal requirements for the elevator control system were given. The following are relevant to our discussion:

1The elevator doors should not be allowed to be opened when the elevator is moving or between floors. This is regarded as a safety requirement;

2When the ‘Emergency’button on the elevator control panel is pressed the elevator should be stopped and the doors opened.

4. Behavioural Conflicts

In section 1.3 we placed behavioural conflicts in their context; they are those inconsistencies, in the specification of behaviour in terms of an consistent entity model, that make it impossible to construct a working system.

We assume that the behavioural specification is free of time-independent logical contradictions. Then, behavioural conflicts occur when two or more behavioural goals can, at some point in time, result in a contradiction. We can classify them as follows:?Application-independent conflicts, in which the possibility of conflict can be seen from the semantics of the causal language, without reference to the application;

?Application-dependent conflicts, in which the conflict depends upon contradictions between predicates in the application;

Since behavioural conflicts are time-dependent, and the applicability of any causal statement is limited by any While clause that qualifies it, the conflicts can only occur during the time intervals in which the While clause holds. Depending upon the clause, it may be possible to evaluate the possibility of conflict statically. If not, timing assumptions will be necessary, as discussed in section 4.1.1, below.

The types of conflict and their means of detection are introduced, before their means of resolution are proposed. At this stage, the means of detection are quite simplistic. We have

primarily focussed our efforts on achieving a means of understanding of the conflict, as this is

a necessary precursor to identifying rigorous methodological guidance.

4.1 Application-Independent Conflicts

In a different context [12] we suggested that the starting point for the detection of policy conflicts is that without some overlap there can be no conflict. The most obvious form of overlap is when two statements refer to the same entity. Given two causal statements: x causal-relation y and z causal-relation w

there are four potential sources of overlap:

?Overlap of subjects, where x and z are the same condition. This does not typically give rise to conflicts, because it is normal for a condition to cause more than one other condition. There are several examples in section 3. We do not discuss these further.?Overlap of objects, where y and w are the same condition. These are discussed in section

4.1.1.

?Overlap of both subjects and objects, where x and z are the same, and y and w are the same, but the linking causal relations are different. These are discussed in section 4.1.2.?Overlap of the object of one statement with the subject of another, i.e. where y and z are the same. These are discussed in section 4.1.3.

We therefore suggest that a first approach to conflict detection should be to scan the specification, making a pairwise comparison of causal statements, to search for the occurrence of potentially conflicting pairs of conditions. These can be examined to decide if they match any of the conflict criteria described below.

4.1.1Overlap of Objects

We can see the possible conflicting causal statements from the following table. Since there is no significance in the order of stating causal laws, we have omitted the lower diagonal:

B directCauses

C B terminates C B sustains C B prevents C

A directCauses C No conflict (a)No conflict (b)No conflict (b)Conflict

A terminates C No conflict (a)Conflict No conflict (b)

A sustains C No conflict (a)No conflict (b)

A prevents C No conflict (a)

Notes:

a)All of the causal statements are idempotent, so no conflicts arise from overlaps on the

diagonal.

b)directCauses and prevents are concerned with the start of the object condition, and

sustains and terminates are concerned with its end, so neither directCauses nor prevents can conflict with sustains or terminates.

The conflicts which may arise are directCauses versus prevents, and terminates versus sustains.

? A directCauses C and B prevents C;

These state that the start of C coincides with the end of A, and that the start of C cannot occur while B holds. If B holds at the end of A there is a contradiction between the two statements, since the definition of directCauses implies that the start of C coincides with the end of A, which is within the interval of B, and the definition of prevents implies that the start of C is not within the interval of B.

? A terminates C and B sustains C. There is a similar contradiction relating to the end of C. An example conflict of this kind is shown in the lift car specification:

StartOf(EmergencyBrakeOn) terminates AccComfort

OccupantSensed sustains AccComfort

Since there is no constraint preventing EmergencyBrakeOn from starting while OccupantSensed holds, there is the possibility of a conflict occurring.

We can generalise the directCauses case to indirectCauses:

? A indirectCauses C and B prevents C;

The reasoning is similar to directCauses. There must be some X such that A indirectCauses X and X directCauses C; if B holds at the end of X there is a conflict, as above.

These possible conflicts need to be detected, and if they can cause an actual run-time conflict it must be resolved before the system is implemented. Jaffe et al [13] point out the difficulties of determining whether they can cause a run-time conflict as this depends on the relative timings of the causing conditions.

4.1.2Overlap of both Subject and Object

One conflict arising from overlap of both subject and object is straightforward to detect and does not require analysis of the semantics of causal statements: complementary object conflicts, e.g. A causal-relation B and A causal-relation ~B. This leads to a conflict because, by the definition of "~", B and ~B cannot hold simultaneously.

We also need to consider the cases when the same two conditions are subject and object of two different causal statements, e.g. A directCauses B and A terminates B. These require more detailed analysis of the semantics of causal statements, which is shown in Appendix A.

A summary of our conclusions from the analysis in the Appendix is:

?Since all the causal statements are idempotent, no conflict arises from the duplication of causal statements, e.g. A directCauses B and A directCauses B.

?No formal logical conflicts arise from any of the combinations examined, which we would expect since the intention in designing them was that their effects should be orthogonal.?Three of the combinations are potentially useful:

?StartOf(A) directCauses B and A sustains B. This is stronger version of sustains which has proved useful in an earlier application [5].

?StartOf(A) directCauses B and A terminates B. This is stronger version of terminates.

?A directCauses B and A terminates B: The net effect is to toggle B at the end of A, so that if B does not hold at the end of A then it will be initiated, and if B does hold at the end of A then it will be terminated. This appears to be a potentially useful combination.

?The remaining combinations are less likely to be useful as components of the language, and some are counter-intuitive in their effects, so they are best regarded as being potentially in conflict with the specifier's intentions.

?Further analysis to include the "~" operator (complementary condition – see section 2.2.3) is not necessary since, as described in section 2.3, we can replace causal statements which include this operator with their equivalents, e.g. replace c directCauses ~d with c terminates d

Overlaps of both Subject and Object therefore also need to be detected, and examined carefully for their effects on the behaviour of the system.

4.1.3Sequential Conflicts

There are potentially conflicts arising from a chain of causal statements, in particular if there are two cycles rotating in opposite directions, e.g.:

A directCauses

B and B directCauses

C and C directCauses A

A directCauses C and C directCauses

B and B directCauses A

It is unlikely that it is possible to construct a useful set of predicates associated with the three conditions which can consistently apply to both cycles.

A cycle occurs in the lift system:

StartOf(Open) terminates Opening

StartOf(Closed) terminates Closing

StartOf(Closing) terminates Open

StartOf(Opening) terminates Closed

This is quite legitimate, and the predicates (the value of Aperture) associated with each condition are consistent. However, a second cycle in the opposite direction would clearly be nonsensical.

Therefore the specification should be scanned for cycles of causes, to ensure that none of them conflict.

4.2 Application-Specific Conflicts

It has been possible to identify the above conflicts without reference to any specific application. However, even if none of these conflicts exist, there may be conflicts which depend upon the application. They arise when causal statements would put the system into two incompatible conditions, e.g. A directCauses AtFloor(1) and A directCauses AtFloor(2) simultaneously. Two conditions are incompatible if their associated predicates are in contradiction.

A directCauses AtFloor(1) and A directCauses AtFloor(2) are incompatible because they have contradictory predicates. We sketch the basis for a proof of this inconsistency, introducing known properties of the application to support it:

?For any n, AtFloor(n) holds only when the elevation of the lift is at the same elevation as Floor(n) since

? t: Time; n: ?? (AtFloor(n)) HoldsAt t ?

(Elevation(t) = (Floors(n)).Elevation ∧ Speed(t) = 0)

?The elevation of every floor is different since

? n1, n2: ? | n1 ≤ 5 ∧ n2 ≤ 5 ?

(n1 > n2) ? ( (Floors(n1)).Elevation > (Floors(n2)).Elevation )

?So

? t: Time ?? ( AtFloor(1) HoldsAt t ∧ AtFloor(2) HoldsAt t )

Occurrences of this type of conflict must be found by inspection as they are dependent upon properties of the application, rather than the syntax of the notation. We can now consider two specific examples of application-specific conflict from our lift example that serve to illustrate the principles.

4.2.1Example 1: Emergency Button Conflict

A more practical example of a conflict is that between requirements 1 and 2 as defined in section 3.3.

The following predicates specify that AtFloor(n) only holds when the car is stationary at the floor n, and AtAFloor holds when AtFloor(n) holds for any n:

? t: Time; n: ?? (AtFloor(n)) HoldsAt t ?

(Elevation(t) = (Floors(n)).Elevation ∧ Speed(t) = 0)

? t:Time ? AtAFloor HoldsAt t ? (? n:?? (AtFloor(n)) HoldsAt t)

Requirement 1 states: The elevator doors should not be allowed to be opened when the elevator is moving or between floors, and is expressed by following safety requirements in the specification:

? n:?? (~AtFloor(n)) prevents (Floors(n)).LandingDoor.Opening

(~ AtAFloor) prevents CarDoor.Opening

(~ CarDoor.Closed) sustains Stationary

Requirement 2 states: When the ‘Emergency’button on the elevator control panel is pressed the elevator should be stopped and the doors opened:

EmergencyButton directCauses EmergencyBrakeOn

EmergencyButton directCauses CarDoor.Opening

These causal statements violate both parts of requirement 1 unless the car is stationary at a floor when the button is pressed.

4.2.2Example 2: Scheduling Conflict

Another, hypothetical, example of a conflict is a scheduling conflict which we introduce in order to illustrate a different method of resolution in section 4.3.1.

An initial specification of requirements for the system might say that pressing a request button directly causes the lift to come:

? n:?? (Requests (n)).FloorReq directCauses MovingToFloor(n)

This statement would not be recognised as potentially leading to a conflict by the scanning methods recommended above if it were the only one whose object was MovingToFloor(n). However, there may be a number of passengers, whose demands for service conflict. The

conflict arises from the fact that the speed predicates associated with the conditions MovingToFloor(0)…MovingToFloor(4) are mutually incompatible.

4.2.3Detecting Conflicts through the Use of a Conflicts Database

In order to search systematically for conflicting conditions, we need to identify those whose predicates may be in contradiction. It is possible in principle to automatically create a database of sets of conditions whose predicates are potentially in conflict. This would ensure thorough coverage, however the size of such a database is likely to be quite large.

If the database were limited to pairwise comparisons, its size would be O(n2), approximately 400 for our example. Unfortunately we cannot limit the inspection to pairwise comparisons. Consider the following:

A directCauses B

A directCauses C

C sustains ~B

Pairwise there is no conflict between the statements. Only together are they problematical, requiring examination of their predicates using knowledge of the application. The inclusion of three-way comparisons would increase the database size to O(n3), approximately 8,000 for our example. There could also be sets of four or more statements creating application conflicts. Therefore, although the concept of a conflicts database is attractive, it will require further work in order to ensure that it can be kept to a manageable size while still ensuring thorough coverage of conflicts, or efficient search strategies employed. We anticipate that for the moment, the most effective means of identifying such conflicts are likely to be through traditional inspection methods (though armed with an increased knowledge of the types of inconsistency), or supported through the kind of animation toolset described in section 6.3. 4.3 Resolution of Conflicts

Having identified conflicts, it is necessary to decide what to do with them. We work within the domain of safety critical systems, and so for us the most desirable solution in the face of conflict is to eliminate it entirely. This is however not always possible, and so we identify two further ways of managing the conflict. The actual acceptability of approach for any particular context must be judged on a case-by-case basis, and depends on the sector within which the technology is applied. The three possible approaches to resolution of conflicts are:

?Total elimination;

?Dynamic elimination;

?Prioritisation.

Elimination, as opposed to prioritisation, implies modifying the conflicting statements so that the conflict cannot occur. This must not, of course, be done unilaterally but has to be negotiated between the stakeholders of the system.

We illustrate the approaches using the two conflicting sets of statements from the lift specification:

EmergencyButton directCauses EmergencyBrakeOn S1 EmergencyBrakeOn directCauses CarDoor.Opening S2

These statements cause the Emergency Brake to bring the car to a halt and then cause the car door to open without reference to whether the car is at a floor. However, we also have the statement:

~AtAFloor prevents CarDoor.Opening S3 This statement prevents the car door from opening unless the car is at a floor. So there is a conflict if the Emergency Button is pressed at any time that will result in the car halting between floors.

4.3.1Total Elimination of a Conflict

The conflict may be totally eliminated so that, regardless of the state of the system, it cannot occur. In the Emergency Button example we could achieve this by completely removing statements S1 and S26.

We can also eliminate the scheduling conflict (section 4.2.2) in the way that was actually done in the specification. If instead of directCauses we use indirectCauses the conflict of predicates is removed. Hence the solution that was adopted, which decoupled the registering of a floor request from the decision to despatch the lift to the floor:

? n:?? (Requests (n)).FloorReq indirectCauses AtFloor(n)

? t: Time ? (? n: ?? (Requests (n)).PreferredReq HoldsAt t )

? n:?? (StartOf (Requests(n)).PreferredReq) directCauses MovingToFloor(n)

4.3.2Dynamic Elimination of a Conflict

We can dynamically eliminate the conflict by modifying the conflicting statements so that they never apply at the same time. In the example above we could achieve this by completely replacing statement S1 with the following:

S4 While AtAFloor

EmergencyButton directCauses EmergencyBrakeOn

Since ~AtAFloor and AtAFloor can never hold simultaneously, the conflict is eliminated.

4.3.3Prioritisation of Conflicting Statements

Alternatively, we can introduce, in advance, methods of resolving the conflict without modifying the conflicting statements, by changing the semantics of the specification language, so that one statement is nullified by the presence of the other. There is then no need to modify the specification.

There are several possible approaches to prioritising conflicting statements, derived from similar conflicts in access control specifications (see, e.g. [14]). Possibilities include:

https://www.wendangku.net/doc/4f5895464.html,belling conditions with explicit priorities, so that e.g. A has priority 1 and B has priority

2, and resolving the conflict on the basis of priorities;

2.Resolving the conflict on a temporal basis, e.g. giving priority to the most recently created

condition occurrence;

6 Actually, we believe that the emergency button was introduced into the requirement by mistake, and this would be our preferred solution.

3.Resolving the conflict on the basis of the source of the requirement, e.g. giving priority to

the most senior stakeholder;

4.Assigning priorities to the causal statements themselves, so that prevents has priority over

causes and sustains has priority over terminates.

Although the first three methods have been discussed in the access control literature, they clearly add complication to the specification, and it may be difficult to predict their effects.

We prefer the last approach, and in our definition of the causal language we give prevents priority over directCauses, and sustains priority over terminates, so that in this example S2 has no effect. We can point to some persuasive arguments in favour of this approach.

Implied in the principle of causality – "nothing happens without a cause" is a hierarchy of behavioural imperatives. The default behaviour of a system is no change:

?Newton's First Law, which applies to the behaviour of physical systems, is that bodies continue in a straight line with uniform speed unless subjected to an external force;?Typically, digital control systems are programmed to maintain their environment in a constant state unless they receive external inputs requiring change.

Any explicit causal imperative for action has priority over the default, and this is the second level of the hierarchy. This suggests a natural third level of hierarchy for the resolution of conflicts – that the explicit prevention of change has priority over imperatives for action. This is similar to the typical hierarchy that is used to resolve conflicts in access control specifications – if the default is negative, positive authorisations override the negative default, and explicit negative authorisations override positive ones. This gives sufficient power in most access control systems to meet all practical access specification needs.

We therefore propose the following hierarchy, in ascending order of priority:

?The default – nothing is specified and nothing changes;

?Positive statements – A directCauses B;

?Negative statements, which will override the positive – A prevents B.

A similar, orthogonal, hierarchy is used for terminates and sustains:

?The default – nothing is specified and nothing changes;

?Positive statements – A terminates B;

?Negative statements, which will override the positive – A sustains B.

This hierarchy does not apply universally. The emergency brake causes greater deceleration than is comfortable:

StartOf EmergencyBrakeOn terminates AccComfort

However, we also have the comfort requirement:

OccupantSensed sustains AccComfort

Our prioritisation gives sustains priority over terminates, but almost certainly this is not what the stakeholders require, so in this case the specification will need to be modified to exclude the case of emergency braking:

[while ~ EmergencyBrakeOn ] OccupantSensed sustains AccComfort

Note that there is an advantage in using prioritisation over explicit removal of conflicts. S4, above, removes the conflict satisfactorily, but it has introduced redundancy into the specification; it for any reason it is necessary to change the statement S3, it will be necessary also to change S4, and anywhere else in the specification that a similar While occurs. Although we have a view on the hierarchy of causal statements, as stated above, we accept that this is by no means settled – with experience it may be necessary to adopt a domain-specific approach to prioritisation of causal statements.

5. Related work

In this section we give some examples of related work dealing with behavioural inconsistencies and conflicts, from two application areas. The field of inconsistency and conflict is very wide, ranging over a large variety of applications, and straying into philosophy; we have limited ourselves to two areas that directly address behavioural inconsistency.

Feature Interactions in Telecommunications Systems

The most conspicuous example of behavioural conflict that has emerged recently is feature interactions in telecommunications systems. This was the subject of special issues of IEEE Computer [15] and IEEE Communications Magazine [16]. An example is the behaviour of Selective Call Rejection in the presence of Call Forwarding, which may result in undesired behaviour. In [17] Zave discusses formal approaches to managing feature interactions, identifying three main approaches: strong typing of features to prevent accidental interactions; specifying system state invariants, e.g. forbidding states in which there is a cycle of call forwarding; and formal specification methods such as the use of finite state automata.

More recently Thomas [7] presents a formal modelling approach to telecommunications services in which she points out that, although a "feature interaction" operator has been used in the literature it has never been formally defined, and goes some way towards its formal definition. Service features are defined as "first-class" concepts and explicit conflicts between them are modelled as logical inconsistencies and resolved by defining orderings between them, using LOTOS. The other source of potential feature interaction is non-determinism, which is captured in the LOTOS model and by the use of the modal μ-calculus for the analysis of timing properties (see the paper for references to these formalities). This appears to be a promising approach to dealing with the problem described in section 4.1.1 above, i.e. determining whether a potential timing conflict will materialise.

Database Integrity Constraints

Work on the enforcement of database integrity constraints is also relevant to behavioural inconsistency, if we regard a database transaction as a form of behaviour. Sheard & Stemple [18] describe a schema notation which, in addition to those constraints which can be expressed directly through an ER diagram, enables the expression of application-specific constraints. They then go on to show how it can be automatically verified that individual transactions conform to these constraints. Plexousakis & Mylopoulos [19] demonstrate an integrity maintenance technique that modifies transaction specifications by incorporating in them conditions necessary to constraint satisfaction, thus eliminating the need for subsequent verification. Techniques such as these could be useful, in a causal specification, for identifying application-independent conflicts and resolving conflicts of all kinds after identification.

6. Conclusions

6.1 Structural Inconsistencies and Behavioural Conflicts.

As we discussed in the introduction, a persuasive case has been made out by Gabbay, Nuseibeh and others for allowing inconsistencies to reside in specifications. The emphasis of their work has been on allowing inconsistency, with rather less discussion of the necessity for its eventual elimination. It is common ground among all concerned that inconsistencies must be removed from systems before they are implemented, with the exception of any facilities that may be provided for run-time resolution, e.g. by interaction with a human operator. However, it is not sufficient to treat all inconsistencies at a single level. The behaviour of a system cannot begin to be described until there is a consistent model of the objects in it. Inconsistencies in the model – we might describe them as structural inconsistencies to contrast them with behavioural conflicts – must be resolved before the behavioural conflicts can be dealt with.

6.2 An Approach to Managing Behavioural Conflicts

We have implied an approach to the management of behavioural conflict in the discussion above, and here we suggest an outline process to do this methodically making use of the causal notation:

?The causal specification language itself can contain a mechanism for conflict resolution.

We provisionally recommend giving priority to prevents and sustains over directCauses and terminates, respectively, but recognise that other methods, such as labelling statements with priorities, may turn out to be more appropriate.

?Structural inconsistencies must be removed before attempting to identify behavioural inconsistencies.

?We have identified four kinds of potential conflict which can be recognised without any knowledge of the application:

?Overlap of subjects;

?Overlap of objects;

?Overlap of both subjects and objects;

?Overlap of the object of one statement with the subject of another.

These can be detected systematically by a pairwise comparison of causal statements in the specification.

?We have also described application-specific conflicts which arise from contradiction between the predicates associated with conditions.

Some, at least, of these can be detected by compiling a conflicts knowledge base, which lists those sets of conditions whose predicates are potentially in conflict with each other because their predicates are related, and systematically checking this for potential conflicts.?Thought needs to be given to the resolution of conflicts:

?Where there is a built-in resolution method, such as prioritisation of causal statements, that resolution may not be correct, and may need to be overridden by explicit modification of the specification;

浅析《诗经》中的方位词“南”及其文化内涵

龙源期刊网 https://www.wendangku.net/doc/4f5895464.html, 浅析《诗经》中的方位词“南”及其文化内涵作者:王春艳 来源:《汉字文化(教育科研卷)》2018年第07期 【提要】本文就《诗经》中出现频率较多的方位词“南”进行辨析,并对具有代表性的“南方”“南亩”“南山”进行具体分析,由此我们可知“南”这一方位词,有着温暖和煦、丰年祈福之愿,有着少妇思君、忧心忡忡之情。随着对“南”与长养、情思、尊愿等方面的分析,可见方位词“南”的文化内涵不断深化并影响深远。通过对方位词“南”的探析,我们可以加深对《诗经》的认识,从而揭开遥远先秦的神秘面纱。 【关键词】诗经方位词“南” 文化内涵 《诗经》作为先秦人民真实的生活写照,其所包含的先民思想、风俗习惯、地理方位等都是我们了解先秦人民生活风貌的重要载体。关于《诗经》中方位词“南”,此前已有学者对此进行研究,譬如张德鑫的《方位词的文化考察》,方经民的《汉语空间方位参照的认知结构经过统计》,金安辉的《诗经》中的“东、西、南、北”及其对后世诗歌的影响等,笔者在前人研究的基础上,旨在更加具体、深刻地分析方位词“南”及其文化内涵。据统计,《诗经》中“南”出现了81次,那么《诗经》中的“南”是仅指方向的方位词呢,还是有着特殊的文化内涵?文化内涵也可以说是文化义,周一农的《词汇的文化蕴涵》中指出“文化义,指的是词在特定文化背景下所获得的反映一个名族风俗习惯、文化背景、宗教信仰和思维方式等诸多文化因素的隐含义”。①因此方位词的文化内涵就是对这些文化因素的分析。下面我们将对《诗经》中的方位词“南”进行逐步探讨,从而还其完整面貌。 一、“南”与长养 万事万物皆有源头,那么方位词源于何处?先秦人民不像现代人一样可以用多种方式指认方向,他们最先感受到的是自身和空间的环境关系,“日出而作,日落而归”,四方就是根据太阳这一参照物来确定的。即太阳升起处定为东方,落下处定为西方,直照处定为南方,背阳处定为北方。这就是人们对方位最初的认识。而我们现在所说的方位词,更加术语化,其实还是指东、西、南、北等。 经统计,我们发现《诗经》中“南”多有表示南方的意思,《说文解字》:“南,木至南方而有枝任也”,即南方是夏天草木繁盛的象征。《诗经》中《周南·樛木》“南有樛木,葛藟累之”;《周南·漢广》“南有乔木,不可休思”;《召南·草虫》“陟彼南山,言采其蕨”这些例子不仅表明这些草木生长在南方,也进一步表明了南方的“樛木”“乔木”“蕨”是何其丰茂,这正如《白虎通·五行》中“南方主长养”的说法,又《黄帝内经·素问·异法方宜论》:“南方,天地所长养,阳之所盛处也”,所以南方是温暖和煦的,也是植物生长的好地方,是生命的象征。

The way常见用法

The way 的用法 Ⅰ常见用法: 1)the way+ that 2)the way + in which(最为正式的用法) 3)the way + 省略(最为自然的用法) 举例:I like the way in which he talks. I like the way that he talks. I like the way he talks. Ⅱ习惯用法: 在当代美国英语中,the way用作为副词的对格,“the way+ 从句”实际上相当于一个状语从句来修饰整个句子。 1)The way =as I am talking to you just the way I’d talk to my own child. He did not do it the way his friends did. Most fruits are naturally sweet and we can eat them just the way they are—all we have to do is to clean and peel them. 2)The way= according to the way/ judging from the way The way you answer the question, you are an excellent student. The way most people look at you, you’d think trash man is a monster. 3)The way =how/ how much No one can imagine the way he missed her. 4)The way =because

insight使用

1.1 建立优化目标 优化目标有两种,一种是测量(measure ),另外一种是目标对象(object )。 1.1.1 测量(measure )的建立 ADAMS 提供多种measure ,如图10.20a 菜单所示,常用的主要由两点之间的测量(point-to- point )和角度的测量(angle )。用户可以通过菜单打开图10.20b 和图10.20c 所示的measure 创建和编辑对话框,完成测量的建立和修改。 图10.20 测量(measure )的建立 a )菜单 d )测量图线 b )两点之间的测量 c )角度的测量

1.1.2 目标对象(object )的建立 通过菜单simulation | Design object 打开如图10.21的目标对象(object )创建和编辑对话框,完成目标对象的建立和修改。 图10.21目标对象(object )的建立 1.2 参数敏感度分析 Step1: 打开ADAMS/Isight 模块 先对模型进行仿真,然后通过菜单Simulation | ADAMS/Isight | Export …,打开分析文件保存对话框如图10.22所示,修改分析文件名后,按OK ,创建分析文件(xml 文件),并进入ADAMS/Isight 模块如图10.23所示。 图10.22 分析文件保存对话框

优化变量 优化目标 优化设置 图10.23 ADAMS/Isight模块界面

Step2:选取优化变量 在窗体左侧选中用于敏感度研究的优化变量,按添加到选取栏如图10.24所示。优化变量选取栏 图10.24 ADAMS/Isight模块界面(优化变量)

介词in,on,to表示方位的用法

介词in,on,to 表示方位的用法 介词 in,on,to 都可以用来表示某个位置的方向,它们的意义不同,故表示的方向及范围也不同: 1. in 表示方位,含义是“在……之内”,即一个小地方处在一个大地方的范围(疆域)之内。例如: China is in the east of Asia. 中国在亚洲东部。(中国是亚洲的一个国家,处于亚洲的范围之内) Guilin is in the north of Guangxi. 桂林在广西北部。(桂林是广西的一座城市) Taiwan lies in the east of China. 台湾在中国的东部。(台湾是中国东部的一个省份,是中国的领土,在中国的疆域之内) Shanghai lies in the east of China. 上海位于中国的东部。(上海是中国的一个行政区域,在中国的疆域之内) The plant can be seen only in the north of Canada. 那种植物只有在加拿大北部才看得到。(暗指这种植物只生长在加拿大北部地区) The sun rises in the east and sets in the west. 太阳东升西落。 说明:表示某个地方的地理位置时,be,lie 以及 be located 的意义是一样的,可以互换使用。 2. on 表示方位,含义是“在……端/边”,即一个地方在另一个地方的某一端或某一边,两个地方只是相邻或接壤,却互不管辖。例如: Guangdong Province is on the southeast of Guangxi. 广东省在广西的东南边。(广东省与广西在地理位置上是连在一起的,即两者相邻,却互不管辖) China faces the Pacific on the east. 中国东临太平洋。(中国与太平洋相邻) The country is bounded on the west by the sea.那个国家西边与海接界。(暗指该国为沿海国家) Sichuan Province is on the north of Guizhou Province. 四川省在贵州省的北边。(四川省与贵州省在地理上也是连在一起的,但互不管辖) 3. to 表示方位,含义是“在……面”,即一个地方在另一个地方的范围之外,互不管辖。尤其当两个地方相隔较远,且有湖泊、大海等区域相隔时,通常用 to。例如: Japan is to the east of China. 日本在中国的东面。(日本在中国范围之外,且有日本海分隔) Taiwan is to the southeast of Fujian Province. 台湾在福建省的东南面。(台湾在福建省的范围之外,且两者之间有台湾海峡分隔) Jinzhou is to the west of Shenyang. 锦州在沈阳的西面。(锦州和沈阳分别为两座城市,地理位置上互不

The way的用法及其含义(二)

The way的用法及其含义(二) 二、the way在句中的语法作用 the way在句中可以作主语、宾语或表语: 1.作主语 The way you are doing it is completely crazy.你这个干法简直发疯。 The way she puts on that accent really irritates me. 她故意操那种口音的样子实在令我恼火。The way she behaved towards him was utterly ruthless. 她对待他真是无情至极。 Words are important, but the way a person stands, folds his or her arms or moves his or her hands can also give us information about his or her feelings. 言语固然重要,但人的站姿,抱臂的方式和手势也回告诉我们他(她)的情感。 2.作宾语 I hate the way she stared at me.我讨厌她盯我看的样子。 We like the way that her hair hangs down.我们喜欢她的头发笔直地垂下来。 You could tell she was foreign by the way she was dressed. 从她的穿著就可以看出她是外国人。 She could not hide her amusement at the way he was dancing. 她见他跳舞的姿势,忍俊不禁。 3.作表语 This is the way the accident happened.这就是事故如何发生的。 Believe it or not, that's the way it is. 信不信由你, 反正事情就是这样。 That's the way I look at it, too. 我也是这么想。 That was the way minority nationalities were treated in old China. 那就是少数民族在旧中

Insight操作指导

西门子Insight软件(服务器)操作指导 ---烟台万达文华酒店 一、开机检查及软件启动 1、在开机之前先检查Echo ID 是否插在主机的USB接口上 2、开机后等到网络连接图标出现叹号后再查看服务是否开启 3、查看相关的服务是否已经开启,需要开启的服务如下图所示: (查看服务方法:右键我的电脑/管理/双击服务和应用程序/双击服务/随便选择一个服务后按I就可以跳转到Insight相关的服务区域) ①右击我的电脑②进入服务选项 ③双击服务后进入服务窗口

④需要开启的服务如上图 4、若以上几个服务有没开启的,需要按照以下方法进行配置: (1)首先将Insight AsyncSvc服务关闭 (2)按照此路径找到baccfg.bat文件(路径:C:\Program Files\Cimetrics\BACstac v6.0g)后双击后点确认,会自动退出。

(3)在开始/所有程序/Insight Version 3里面找到LocalNet选项,单击进入后勾选第2和5,点击确定就可以。 ( (4)将现有权限删除掉: 根据下面路径进入C:\Program Files\Siemens\APOGEE\Common,在这个文件夹里面会有很多.bat/.exe的文件,只需要找到“Del_lic.bat”文件,双击就可以将现有权限删除 (5)给软件重新授权: 先将厂家提供的“狗文件”(就是那个TXT文档),先复制到Common目录下,根据提示,直接选择替换就可以,然后将此TXT文档,拖到“ApogeeLicense.bat”文件上就可以了,会出现一个DOS窗口,完成后按任意键就可以了。

(完整版)the的用法

定冠词the的用法: 定冠词the与指示代词this ,that同源,有“那(这)个”的意思,但较弱,可以和一个名词连用,来表示某个或某些特定的人或东西. (1)特指双方都明白的人或物 Take the medicine.把药吃了. (2)上文提到过的人或事 He bought a house.他买了幢房子. I've been to the house.我去过那幢房子. (3)指世界上独一无二的事物 the sun ,the sky ,the moon, the earth (4)单数名词连用表示一类事物 the dollar 美元 the fox 狐狸 或与形容词或分词连用,表示一类人 the rich 富人 the living 生者 (5)用在序数词和形容词最高级,及形容词等前面 Where do you live?你住在哪? I live on the second floor.我住在二楼. That's the very thing I've been looking for.那正是我要找的东西. (6)与复数名词连用,指整个群体 They are the teachers of this school.(指全体教师) They are teachers of this school.(指部分教师) (7)表示所有,相当于物主代词,用在表示身体部位的名词前 She caught me by the arm.她抓住了我的手臂. (8)用在某些有普通名词构成的国家名称,机关团体,阶级等专有名词前 the People's Republic of China 中华人民共和国 the United States 美国 (9)用在表示乐器的名词前 She plays the piano.她会弹钢琴. (10)用在姓氏的复数名词之前,表示一家人 the Greens 格林一家人(或格林夫妇) (11)用在惯用语中 in the day, in the morning... the day before yesterday, the next morning... in the sky... in the dark... in the end... on the whole, by the way...

Source Insight用法精细

Source Insight实质上是一个支持多种开发语言(java,c ,c 等等) 的编辑器,只不过由于其查找、定位、彩色显示等功能的强大,常被我 们当成源代码阅读工具使用。 作为一个开放源代码的操作系统,Linux附带的源代码库使得广大爱好者有了一个广泛学习、深入钻研的机会,特别是Linux内核的组织极为复杂,同时,又不能像windows平台的程序一样,可以使用集成开发环境通过察看变量和函数,甚至设置断点、单步运行、调试等手段来弄清楚整个程序的组织结构,使得Linux内核源代码的阅读变得尤为困难。 当然Linux下的vim和emacs编辑程序并不是没有提供变量、函数搜索,彩色显示程序语句等功能。它们的功能是非常强大的。比如,vim和emacs就各自内嵌了一个标记程序,分别叫做ctag和etag,通过配置这两个程序,也可以实现功能强大的函数变量搜索功能,但是由于其配置复杂,linux附带的有关资料也不是很详细,而且,即使建立好标记库,要实现代码彩色显示功能,仍然需要进一步的配置(在另一片文章,我将会讲述如何配置这些功能),同时,对于大多数爱好者来说,可能还不能熟练使用vim和emacs那些功能比较强大的命令和快捷键。 为了方便的学习Linux源程序,我们不妨回到我们熟悉的window环境下,也算是“师以长夷以制夷”吧。但是在Window平台上,使用一些常见的集成开发环境,效果也不是很理想,比如难以将所有的文件加进去,查找速度缓慢,对于非Windows平台的函数不能彩色显示。于是笔者通过在互联网上搜索,终于找到了一个强大的源代码编辑器,它的卓越性能使得学习Linux内核源代码的难度大大降低,这便是Source Insight3.0,它是一个Windows平台下的共享软件,可以从https://www.wendangku.net/doc/4f5895464.html,/上边下载30天试用版本。由于Source Insight是一个Windows平台的应用软件,所以首先要通过相应手段把Linux系统上的程序源代码弄到Windows平台下,这一点可以通过在linux平台上将 /usr/src目录下的文件拷贝到Windows平台的分区上,或者从网上光盘直接拷贝文件到Windows平台的分区来实现。 下面主要讲解如何使用Source Insight,考虑到阅读源程序的爱好者都有相当的软件使用水平,本文对于一些琐碎、人所共知的细节略过不提,仅介绍一些主要内容,以便大家能够很快熟练使用本软件,减少摸索的过程。 安装Source Insight并启动程序,可以进入图1界面。在工具条上有几个值得注意的地方,如图所示,图中内凹左边的是工程按钮,用于显示工程窗口的情况;右边的那个按钮按下去将会显示一个窗口,里边提供光标所在的函数体内对其他函数的调用图,通过点击该窗体里那些函数就可以进入该函数所在的地方。

表示方位的介词用法

Montrer et situer les objets 1.Les mots pour situer les objets. a.contre对着,朝着 b. sur 在…上空 c. a droite (de)在…右边 d. a gauche (de)在…左边 e. sous 在…下面 f. dans在…里面 g. a cote (de)在…旁边h. derriere在…后面i. devant 在…前面 j. au-dessus 在…上方k. au-dessous 在…下方l. entre 在…中间 m. en face de 在…对面n. au bout de 在…尽头o. pres de 在…附近 2.Les mots Cles. a.Vous arrivez 您到达 b. vous prenez 您乘 c. vous allez 您去 d. passez您经过 e. continuez 继续走 f. traversez 穿过 g. tournez 转弯h. entrez走进…i. tout droit 直走 https://www.wendangku.net/doc/4f5895464.html, rue 那条路k. par la从那边 3.Transport. a. A pied 走路 b. avelo骑自行车 c. a moto 骑摩托车 d. en rollers滑旱冰 e. en bus 乘公交车 f. en metro乘地铁 g. en voiture 乘汽车h. en taxi乘出租车 -Comment y aller ? -C’est loin. -?a se trouve près d’ici. -C’est situé à 20km de Paris. -Je suis perdue. Je cherche la rueBotonnet pour aller.....vous pouvez m’indiquer....par où il faut passer pour aller à -C’est de quel c?té? Dans quelle direction ? -Continuez jusqu’à un café qui est au bout de la rue. -Vous suivez la Seine. -Vous traversez la rue et passez devant la poste. -C’est à 5 min à pied . -Vous prenez la première à gauche, tout droit.

英语方位词知识分享

英语方位词的用法 (一)in the east 与 on the east的区别 1.in the east表示我们生活中和地理位置上的绝对方向。如: The sun rises in the east and sets in the west. 太阳从东边升起,从西边落下。 The Great Wall begins in the east from the Shanghaiguan Pass and ends at the Jiayu guan Pass in the west. 长城东起山海关,西至嘉峪关。 2.on the east表示某事物位于另一事物所朝的方向。这里的方向是相对而言的。如: China faces the Pacific on the east. 中国东临太平洋。 The United States faces the Atlantic on the east and the Pacific on the west. 美国东临大西洋,西濒太平洋。 (二) in (to,on,at) the east of 1.要表示A在B的东部,即:A在B的范围之内时就用"A is in the east of B",如: Japan is in the east of Asia.日本在亚洲东部。 Italy is in the south of Europe.意大利在欧洲南部。 2.如果A在B的东方,即:A在B的范围之外,且相隔有一定的距离,就用"A lies to the east of B".口语中有时可将to the省去。如: Japan lies (to the) east of China.日本位于中国东方。 France lies (to the) east of England.法国位于英国东方。 3.如果A在B的东边(侧),即:A与B相邻接。就用"A is on the east of B". 如: Guangdong is on the south of Hunan.广东在湖南南边。

昆明大观楼长联的语言文化内涵探析

昆明大观楼长联的语言文化内涵探析 大观楼位于风景秀丽的昆明西南郊滇池畔,建于康熙二十九年。大观楼四周视野开阔,滇池烟波浩渺,从西山俯瞰,大观楼掩映在湖光山色之间,可谓洋洋大观,故取名大观楼。大观楼自建成后便成了省城第一名胜,吸引了众多的文人墨客来此吟诗作画。其中乾隆年间著名寒士孙髯翁超凡脱俗,所撰写的大观楼长联堪称一绝,被后人誉为古今第一长联,大观楼也因此而扬名天下。孙髯,字髯翁,祖籍陕西三原,幼时随父入滇,天资聪颖,年轻时参加童试,因不愿受其搜身之辱,便愤然离去,从此不复参加科举考试,终生为布衣。髯翁博学多识,却贫困潦倒一生,晚年只能靠卖卜为生。他所作的大观楼长联上下联共180字,就字数而言,并不是最长者,但就思想意义和对后世的影响而论,大观楼长联古今第一的美誉实至名归。关于此联的艺术成就,前人已经做过很多的研究,但就文化内涵而言,前人涉及较少,所以本文试从语言特色和文化内涵两个方面,对长联进行剖析和解读。 一.大观楼长联的语言特色 对联是中国独特的文学艺术形式,它始于五代,盛于明清,迄今已有一千多年的历史。对联一般应该具备四个要素,一是字数相等,断句一致。但也有一些例外的情况,如民国时期有这样一幅对联,上联是袁世凯千古,下联为中国人民万岁,这副对联意在讽刺袁世凯,虽然上下联字数不等,却很符合当时中国人民的心声,所以也被接受和广泛传诵。二是平仄相合,音调和谐。对联要求上下联平仄要对应,传统习惯是仄起平收,即上联末句尾字用仄声,下联末句尾字用平声。三是要求词性相对,位置相同。一般称为虚对虚、实对实,即虚词对虚词,实词对实词。四是要求内容要相关,上下衔接。髯翁所作的大观楼长联立意高远,气势磅礴,除了具备对联的基本要素之外,在语言运用上也颇具特色,值得玩味。 (一)长联多种修辞手法的运用 长联巧妙地运用了排比、比喻、拟人等多种修辞手法,使之气势如虹,意境深远,为长联增色不少。 1.比喻修辞手法的巧妙运用 长联中巧妙地运用了比喻修辞手法,比如看东骧神骏,西翥灵仪,北走蜿蜒,南翔缟素联中就用神骏来比喻昆明东边的金马山;灵仪喻西面的碧鸡山;用蜿蜒来形容北面的长虫山;缟素喻南面的白鹤山。这样一来,就把滇池四周静态的山脉描写得活灵活现,再加上前边的看字,一幅充满生机的画面立刻展现在人们的面前,看吧:东边的金马山似神马奔驰,西边的碧鸡山像凤凰飞舞,北面的长虫山如灵蛇蜿蜒,南端的白鹤山如白鹤翱翔。此外,上联中还用蟹屿螺洲比喻滇池中沙洲的独特形状,用风鬟雾鬓比喻岸边摇曳多姿的垂柳。 2.排比修辞手法的精妙运用 长联中排比修辞手法的运用尤为突出。如东骧神骏,西翥灵仪,北走蜿蜒,南翔缟素,作者在描绘这些自然景物时,运用了空间排比的手法,将东、西、南、北四个方位词运用到句子中,构成排比句。汉习楼船,唐标铁柱,宋挥玉斧,元跨革囊,作者在概括这些历史事件时,运用了时间排比的手法,把发生在云南的历史大事按朝代顺序排列。再如上联莫辜负:四围香稻,万顷晴沙,九夏芙蓉,三春杨柳。下联只赢得:几杵疏钟,半江渔火,两行秋雁,一枕清霜。运用了景物排比和数字排比。作者并不局限于一物,而是眼观八方,笔落四面,把所看到的香稻、晴沙、芙蓉、杨柳逐一排列,并与下联的疏钟、渔火、秋雁、清霜等景物形成对仗。分别用明朗和清冷的色彩词把整个滇池周边的景物完美地呈现在读者面前。同时作者还巧妙地运用了四、万、九、三等数字排比,使长联读起来更具有节奏感。 3.典故的恰当运用 用典是指在作品中引用古人的话语或把历史故事概括说出来的一种修辞手法,用典可以使文章更加凝练。用典也是大观楼长联语言的一大特色,像汉习楼船出自《史记·平淮书》,历史史实是:汉武帝为了攻打云南滇池周边的少数民族,于是在长安大修昆明池,治

“the way+从句”结构的意义及用法

“theway+从句”结构的意义及用法 首先让我们来看下面这个句子: Read the followingpassageand talkabout it wi th your classmates.Try totell whatyou think of Tom and ofthe way the childrentreated him. 在这个句子中,the way是先行词,后面是省略了关系副词that或in which的定语从句。 下面我们将叙述“the way+从句”结构的用法。 1.the way之后,引导定语从句的关系词是that而不是how,因此,<<现代英语惯用法词典>>中所给出的下面两个句子是错误的:This is thewayhowithappened. This is the way how he always treats me. 2.在正式语体中,that可被in which所代替;在非正式语体中,that则往往省略。由此我们得到theway后接定语从句时的三种模式:1) the way+that-从句2)the way +in which-从句3) the way +从句 例如:The way(in which ,that) thesecomrade slookatproblems is wrong.这些同志看问题的方法

不对。 Theway(that ,in which)you’re doingit is comple tely crazy.你这么个干法,简直发疯。 Weadmired him for theway inwhich he facesdifficulties. Wallace and Darwingreed on the way inwhi ch different forms of life had begun.华莱士和达尔文对不同类型的生物是如何起源的持相同的观点。 This is the way(that) hedid it. I likedthe way(that) sheorganized the meeting. 3.theway(that)有时可以与how(作“如何”解)通用。例如: That’s the way(that) shespoke. = That’s how shespoke.

方位名词的特殊用法及其文化本源_王刚

西北民族大学学报(哲学社会科学版)中国民族学类核心期刊2008年第4期J.NORTHWEST UNIVERSITY FOR NATIO NALITIES(Phi losophy a nd Social Science)No.4.2008方位名词的特殊用法及其文化本源 王刚 (北方民族大学国有资产管理处,宁夏银川750021) [摘要]古今汉语方位词没有大的差异,一般很少单独充当句子成份,往往和其他名词结合,表示时间、方位等。由于方位词意义的纷繁复杂,有些方位词在特定的语言环境中,已经脱离了定位的原义,含有特定的意义了。人们对方位的认识,不是单一的表象,是主从统一观,时空统一观、对立统一观的结晶,是在一定的思维文化模式指导下产生的。 [关键词]方位词;特殊用法;文化本源 [中图分类号]H03[文献标识码]A[文章编号]1001-5140(2008)04-0091-04 一 方位词是表示方向和事物相对位置的词,它基本上属于名词的范畴。古今汉语方位词没有大的差异,主要有/东、西、南、北、上、中、下、内、外、前、后、左、右、间、旁0等。方位词一般很少单独充当句子成份,往往和其他名词结合,表示时间、方位等。古今汉语方位词在构成上都有这样一些特征:方位词前都可以加上/之0、/以0构成前加式结构,如/以上、以下、以前、以后、以东、以西、以里、以外0,/之上、之下、之左、之右、之南、之北、之内、之外、之中、之间0等。方位词还可以成对并列联用,如/上下、左右、前后、里外、东西、南北、中间0等。方位词可以直接加在名词前后,如古汉语中/上赏、中赏、下赏、上宾、下人、车左、车右0等,以及现代汉语中/上士、中士、下士、上将、中将、上校、中尉、上级、下级、里屋、外屋、上房0等。人们因生产、生活的需要,很早就有了平面方位的概念,继而又获得立体空间的概念,我们现在经常使用的东、西、南、北、上、中、下等方位词,早在甲骨文中就已经出现,它体现出了古人的方位空间观。关于/东0,5说文6曰:/东,动也,从木。官溥说:从日在日木。0按许慎的说法,/东0是由/日0和/木0组合而成。/日0升到树木的半中腰,表示东方。这种说法未免有点意合。在甲骨文中,/东0像两头扎起来的一个大口袋,它的本义就是代表/东西0(物)。/东0作/东方0讲,是假借之理。因为古时候主人之座在东,宾客之位在西,所以主人称为/东0,如/作东0、/东家0等,/东0就获得了方位的概念。这种观念的确立和古人崇尚礼仪的思维文化模式是相一致的。关于/南0,5说文6认为,/草木至南方而有枝任也。05段注6载,/南,任也,与东、动也一例。古南、男二字相假借。05徐笺6记,/古音南任相近,古南夷之乐曰任。0看来,/南0之为方位词也属于同音假借之理。关于/西0,5说文6曰:/西,鸟在巢上,象形。日在西方而鸟栖。0古文因以为,东西之西,/西0的本义就是/栖0。上古根本就没有/栖0字,而要表示/栖0的意思时就写/西0。至于/西0表示方位,也是假借之理,它和鸟栖的时间有关,是时间和空间的统一观。关于/北0, 5说文6解释为二人相背,这是它的本义。至于用/北0表示方位,同样属于假借之理。北和南是相对立的,古人建屋多南向,则南方为前,北方为后,人们常向南背北,这就产生了北方的概念,这是辨证对立统 [收稿日期]2008-05-07 [作者简介]王刚(1962))男,北京市人,副教授,主要从事古代汉语教学和研究。

way 用法

表示“方式”、“方法”,注意以下用法: 1.表示用某种方法或按某种方式,通常用介词in(此介词有时可省略)。如: Do it (in) your own way. 按你自己的方法做吧。 Please do not talk (in) that way. 请不要那样说。 2.表示做某事的方式或方法,其后可接不定式或of doing sth。 如: It’s the best way of studying [to study] English. 这是学习英语的最好方法。 There are different ways to do [of doing] it. 做这事有不同的办法。 3.其后通常可直接跟一个定语从句(不用任何引导词),也可跟由that 或in which 引导的定语从句,但是其后的从句不能由how 来引导。如: 我不喜欢他说话的态度。 正:I don’t like the way he spoke. 正:I don’t like the way that he spoke. 正:I don’t like the way in which he spoke. 误:I don’t like the way how he spoke. 4.注意以下各句the way 的用法: That’s the way (=how) he spoke. 那就是他说话的方式。 Nobody else loves you the way(=as) I do. 没有人像我这样爱你。 The way (=According as) you are studying now, you won’tmake much progress. 根据你现在学习情况来看,你不会有多大的进步。 2007年陕西省高考英语中有这样一道单项填空题: ——I think he is taking an active part insocial work. ——I agree with you_____. A、in a way B、on the way C、by the way D、in the way 此题答案选A。要想弄清为什么选A,而不选其他几项,则要弄清选项中含way的四个短语的不同意义和用法,下面我们就对此作一归纳和小结。 一、in a way的用法 表示:在一定程度上,从某方面说。如: In a way he was right.在某种程度上他是对的。注:in a way也可说成in one way。 二、on the way的用法 1、表示:即将来(去),就要来(去)。如: Spring is on the way.春天快到了。 I'd better be on my way soon.我最好还是快点儿走。 Radio forecasts said a sixth-grade wind was on the way.无线电预报说将有六级大风。 2、表示:在路上,在行进中。如: He stopped for breakfast on the way.他中途停下吃早点。 We had some good laughs on the way.我们在路上好好笑了一阵子。 3、表示:(婴儿)尚未出生。如: She has two children with another one on the way.她有两个孩子,现在还怀着一个。 She's got five children,and another one is on the way.她已经有5个孩子了,另一个又快生了。 三、by the way的用法

英语方位词的用法

英语方位词的用法 The Standardization Office was revised on the afternoon of December 13, 2020

英语方位词的用法 (一)in the east 与 on the east的区别 1.in the east表示我们生活中和地理位置上的绝对方向。如: The sun rises in the east and sets in the west. 太阳从东边升起,从西边落下。 The Great Wall begins in the east from the Shanghaiguan Pass and ends at the Jiayuguan Pass in the west. 长城东起山海关,西至嘉峪关。 2.on the east表示某事物位于另一事物所朝的方向。这里的方向是相对而言的。如: China faces the Pacific on the east. 中国东临太平洋。 The United States faces the Atlantic on the east and the Pacific on the west. 东临大西洋,西濒太平洋。 (二) in (to,on,at) the east of

1.要表示A在B的东部,即:A在B的范围之内时就用"A is in the east of B",如: Japan is in the east of Asia.在亚洲东部。 Italy is in the south of Europe.在欧洲南部。 2.如果A在B的东方,即:A在B的范围之外,且相隔有一定的距离,就用"A lies to the east of B".口语中有时可将to the省去。如: Japan lies (to the) east of China.日本位于中国东方。 France lies (to the) east of England.位于英国东方。3.如果A在B的东边(侧),即:A 与B相邻接。就用"A is on the east of B". 如:Guangdong is on the south of Hunan.广东在湖南南边。Shangdong is on the north of Jiangsu.山东在江苏北边。4.如果把方位词当作一个整体看,或是看成一点,就用"A is at the east of B" 如:There was a big battle at the north of the Liaodong Peninsula.在辽东半岛的北边有一场大战。5.如果要表示“A 位于B东面100公里处”时我们既可以说"A lies l00km to the east of B",也可以说"A lies 100km east of B". 后者在美国口语中更为常见。如:The plane crashed 30 miles south of the city.飞机在离城南30英里处坠毁。Suzhou lies 50 miles to the west of Shanghai.苏州位于上海西面50英里处。 (三) 汉语里“东南西北”的先后顺序到英语里就变成了north,south,east,west;并由此有了下列中、英文表达上的差异。东南方:southeast 西南方:southwest西北方:northwest 东北方:northeast如:十三陵位于北京西北50公里处。The Ming Tombs are located about 50 km to the northwest of Beijing.天津位于北京东南120公里处。Tiajin is situated l20 km southeast of Beijing.(四)要表示方位的“偏向”时通常用by 正东偏北: east by north正南偏西: south by west正北偏东: north by east正南偏东: south by east如:We are sailing in the direction of

The way的用法及其含义(一)

The way的用法及其含义(一) 有这样一个句子:In 1770 the room was completed the way she wanted. 1770年,这间琥珀屋按照她的要求完成了。 the way在句中的语法作用是什么?其意义如何?在阅读时,学生经常会碰到一些含有the way 的句子,如:No one knows the way he invented the machine. He did not do the experiment the way his teacher told him.等等。他们对the way 的用法和含义比较模糊。在这几个句子中,the way之后的部分都是定语从句。第一句的意思是,“没人知道他是怎样发明这台机器的。”the way的意思相当于how;第二句的意思是,“他没有按照老师说的那样做实验。”the way 的意思相当于as。在In 1770 the room was completed the way she wanted.这句话中,the way也是as的含义。随着现代英语的发展,the way的用法已越来越普遍了。下面,我们从the way的语法作用和意义等方面做一考查和分析: 一、the way作先行词,后接定语从句 以下3种表达都是正确的。例如:“我喜欢她笑的样子。” 1. the way+ in which +从句 I like the way in which she smiles. 2. the way+ that +从句 I like the way that she smiles. 3. the way + 从句(省略了in which或that) I like the way she smiles. 又如:“火灾如何发生的,有好几种说法。” 1. There were several theories about the way in which the fire started. 2. There were several theories about the way that the fire started.

Insight 操作介绍13_COMND

第13章点的命令控制149 循序渐进 点的命令控制 对单点的命令控制就是利用Commander的人工控制来替代Insight的系统程序指令,对输出点(或虚拟输入点)进行控制。点的控制命令将点的命令优先级从None(无)变为OPER(操作员)、SMOKE(烟气)、EMER(紧急)、或PDL(高峰需求限制)。 单点命令控制 1. 在Insight主菜单中,选择Command (指令器)按钮; 则Object Selector(对象选择器)打开。 2. 在对象选择器中选择准备进行命令控制的点,并选择OK 。 则Commander(指令器)窗口打开,并根据所选择点的类型,显示其必要的字段。点的名称被显示在Point Name(点名称)字段中。 3. 在Commander(指令器)窗口中,进行必要的修改操作。有关窗口中各字段的具体定义,请参见窗 口说明一节的内容。 4.当完成窗口中的修改操作之后,选择如下之一的操作: ●选择Command(命令),启动对显示在点名称字段中的点的命令控制。您的命令状态被显示在 Command Status(命令状态)字段中。如果命令成功,则该字段中的信息反映出新调用的命令。 如果命令失败,则在Command Status(命令状态)字段显示一个红叉标记。如果想了解有关错误的说明,可以双击这个红叉标记。 如果完成了点的命令控制,则可以选择Close(关闭)。则Commander窗口关闭,显示返回到Insight 主菜单。 ●如果要对另一个点实施命令控制,则不要关闭Commander窗口,可以在Point Name(点名称)字 段中输入一个新的点名称,然后选择确定。当新的Commander窗口打开时,对该点进行命令控制。 您也可以通过显示Object Selector(对象选择器)窗口来选择一个点。当Object Selector(对象选择器)窗口打开时,选择一个点,然后选择OK。当新的Commander窗口打开时,对该点进行命令控制。 注意:不要忘记将被命令控制的点的控制权还给系统控制,即将其命令优先级恢复到NONE(无)。忘记将点的命令优先级恢复到NONE(无)是引发系统故障的最常见原因。

相关文档