文档库 最新最全的文档下载
当前位置:文档库 › Status Draft Confidentiality Restricted

Status Draft Confidentiality Restricted

OMEGA

Correct Development of Real-Time Embedded Systems

IST-2001-33522

Title :Assertion Languages for Object Structures in UML Author(s) :Marcel Kyas (CAU) and Frank de Boer (CWI)

Editor :CAU

Date :09/01/2003

Identifier :IST/33522/WP1.2/D1.2.1

Document Version :5

Status :Draft

Confidentiality :Restricted

Abstract :We describe five languages for writing expressions,conditions,

constraints,and assertions in UML models.Each of these languages is

an extended subset of OCL,extended to write time constraints and to

describe the architecture of a system.They are used as an expression

language in models and the action language,as a constraint language

describing the relation between objects of a model,or as a

specification language describing the behaviour of objects and

components.We describe the syntax and semantics of these

languages.We define stereotypes enabling better type checking of

constraints and their use and an exchange format is defined.

Docoment History

Version Date Author Comments

509.01.03Marcel Kyas, Frank de Boer Corrections

420.12.02Marcel Kyas, Frank de Boer Corrections

306.12.02Marcel Kyas, Frank de Boer Refined Proposal, Problems of OCL

212.06.02Marcel Kyas, Frank de Boer Corrections

105.06.02Marcel Kyas, Frank de Boer Initial Proposal

1. Deliverable Introduction

This deliverable describes the syntax and semantics of our extension of OCL,which we call ASO (assertion language for object structures).

OCL and ASO reasons about the structure of the states of the system,possibly including path histories.OCL and ASO can be used as a general expression language within the Omega UML language.Whenever assertions on the structure of states and its history are needed in an UML model,they can be expressed in ASO.OCL may be used to specify the internal and observable behaviour of objects and the internal and observable behaviour of components. For the specification of observable behaviours we use an assertion language on the history of observable events. The internal behaviour is specified using sequences of states.

Since the first mile stone,ASO has been redesigned to improve compatibility with OCL 2.0.Most constraints expressed in OCL are constraints in ASO.The language constructs of ASO contain the events and time mechanisms described in deliverable D1.1.2dealing with the real-time extension of UML, for completeness and selfcontainedness of the document. We have analysed possible type systems for OCL and their extension.Despite our initial concerns with OCL's type system,we have decided to use a solution that is compatible with current object oriented programming languages,because other solutions cause more problems than they solve.

Our variant of OCL does not allow specification of liveness properties;to do this,OCL may be used in protocol state machines and live sequence charts.

Assertion Languages for Object Structures in

UML

Marcel Kyas

Frank S.de Boer

January9,2003

Contents

1Introduction4

1.1Relation to the Omega Project (4)

1.2Relation to the Uni?ed Modelling Language (5)

1.2.1UML Class Diagrams (5)

1.2.2UML State Machines (5)

1.2.3Sequence Diagrams (6)

1.2.4The Object Constraint Language (6)

1.3Design Aims (6)

1.4The Semantic Model (8)

1.5Roadmap (8)

2OCL Issues10

2.1Type System (10)

2.1.1Object-Oriented Type System (11)

2.1.2Navigation and Types (11)

2.1.3Parameterisation (11)

2.1.4Inheritance (12)

2.1.5Access Modi?ers (12)

2.2Semantics (12)

2.2.1Ill-de?ned Three Valued Logic (12)

2.2.2Equality (15)

2.2.3Fix-point Semantics (16)

2.2.4Flattening (16)

2.2.5The Meaning of@pre (16)

2.2.6Executability (17)

2.3Usability (18)

2.4Summary and Conclusion (18)

3Logical and Mathematical Foundations20

3.1Formal Model (20)

3.1.1Formal Languages (20)

3.1.2Partial Membership Logic (22)

3.1.3Class Diagrams (23)

3.1.4Object Diagrams (25)

3.1.5Navigation (26)

3.2Recursive De?nitions (27)

3.3Type Theory (28)

3.4Summary (28)

1

4Abstract Syntax30

4.1Types (30)

4.2Expressions (31)

4.3Assertions (31)

4.4Context Declarations (32)

4.5Summary and Comparison to OCL (33)

5Semantics of ASO34

5.1Assumptions (34)

5.1.1Granularity of Steps (34)

5.1.2States (35)

5.1.3History of Events (36)

5.2Invariants (36)

5.2.1Class Invariants (36)

5.2.2Component Invariants (37)

5.3Pre-and Postconditions (37)

5.4Expressions and Assertions (38)

5.4.1Expressions (38)

5.4.2Assert Statement (38)

5.4.3Assertions in State Diagrams (38)

5.5Summary (39)

6Prede?ned Data Types40

6.1Elementary Data Types (40)

6.1.1Booleans (41)

6.1.2Real (42)

6.1.3Integers (42)

6.1.4String (42)

6.2Logical Data Types (43)

6.2.1Any (43)

6.2.2Unit (43)

6.2.3Void (44)

6.3Basic Collections (44)

6.3.1Collection (44)

6.3.2Bag (45)

6.3.3Set (46)

6.3.4Sequence (47)

6.4Iterating Collections (48)

6.4.1Prede?ned Iterators on Sequences (48)

6.4.2Prede?ned Iterators on Bags (49)

6.4.3Prede?ned Iterators on Sets (49)

6.4.4Prede?ned Iterators on Collections (49)

6.5Time (50)

6.5.1Time (50)

6.5.2Duration (51)

6.6Messages and Events (51)

6.6.1Communication Record (51)

6.6.2Signal Events (53)

6.6.3Call Event (53)

6.6.4Object Creation (54)

2

6.7Histories (54)

6.8Summary (55)

7Annotating UML Diagrams56

7.1The Expression Language Fragment (57)

7.2Intra-Object Speci?cation (58)

7.2.1Class Diagrams (58)

7.3Inter-Object Speci?cation (59)

7.3.1Life Sequence Charts (61)

7.3.2State Machines (61)

7.4Intra-Component Speci?cation (62)

7.5Inter-Component Speci?cation (62)

7.6Summary (63)

8Summary and Future Work64

8.1Summary (64)

8.2Future Work (64)

A Interchange Format and Concrete Syntax66

A.1Keywords and Literals (66)

A.2Common Rules (68)

A.3Files (68)

A.4Expressions (69)

A.5Stereotypes (71)

A.6Constraint Interchange (72)

3

Chapter1

Introduction

In this report we describe the abstract syntax and semantics of our assertion language for object structures in the uni?ed modelling language(UML).In par-ticular we will

?We de?ne an extension of the Object Constraint Language(OCL)for re-quirements speci?cation of architectures.

?We de?ne a formal semantics which will be a basis for veri?cation(see work package2.2in[32]).

?We de?ne a package of data types for constraining class diagrams,for behavioural speci?cations,and for requirements speci?cation of architec-tures.

?We de?ne a concrete syntax for tool support and de?ne an interchange format within the XMI.

During the development of the extension of OCL we discovered,that OCL has a number of features which do not serve our purposes.These are described in Chapter2.Our language removes most of these features.To avoid confusion,we therefore call our modi?ed and extended version of OCL an assertion language for object structures(ASO).In this report we describe the syntax and semantics of ASO.

In this chapter we de?ne the purpose and the context of ASO.We describe the structure of this report and the conventions used.

1.1Relation to the Omega Project

Omega aims at the de?nition of a development method in UML for embedded and real-time systems based on formal techniques used to improve commercially available UML tools.In this report we de?ne a formal language for requirements speci?cations of architectures.These requirements are de?ned in UML class diagrams expressed in the Omega kernel language as de?ned in[12].The main di?erences to[12]are:

?The description of a model is based on the UML meta model,as described in[2].Our formalism is by this more abstract than the one presented in[12].

4

?We have integrated the notion of time and event from[18].This step enables us to use a proof method similar to the one presented in[20].

?We have de?ned a syntax for the interchange format proposed in Omega[28].

A second format is also described,similar to the format of OCL con-

straints.

?Both ASO and OCL are languages about state properties.It is similar to assertions in Hoare style veri?cation.We have added a history variable for events which is automatically updated.This could also be achieved by augmenting the original program.For lifeness properties we suggest using Live Sequence Charts[23]or Protocol State Machines.

1.2Relation to the Uni?ed Modelling Language The description of the formal semantics of the UML and ASO uses the UML meta-model as de?ned in[1]and[2].We considered the UML TM Pro?le for Schedulability,Performance,and Time Speci?cation[31]for our model of time. Our work started as an extension of OCL1.4[30],then we changed to OCL

2.0[5],but?nally we found that OCL had many properties which make its use for machine-aided veri?cation di?cult.These issues are addressed in Chap-ter2.Instead,we have decided to create a language which is similar to OCL, but breaks the syntax,wherever the semantics of OCL and our language are di?erent.

1.2.1UML Class Diagrams

UML class diagrams de?ne the structure of a system and thus de?ne the vari-ables and signatures of an ASO formula.This implies that each ASO formula is connected to a class diagram in that an assertion is always evaluated in the context of instances of a class diagram.A model often consists not of only one class diagram but of a collection of class diagrams,each of them modelling a speci?c aspect of the model.In each model di?erent aspects of the used classes are shown.For example,the de?nition of certain classes of the UML meta model is spread over a collection of class diagrams,each of them showing the information relevant to the model.The normative text1on the semantic of a class diagram collects the members de?ned in each class diagram.

Our assertion language is able to handle this aspect speci?c modelling.The semantics of the assertion language allows assertions on incomplete class dia-grams(in the sense that not all members of a class are shown in a class diagram). We hope to suggest methods which will help to identify inconsistencies that arise from the speci?cation of a class in di?erent class diagrams.

1.2.2UML State Machines

The behaviour of a system in UML is modelled using UML state machines.Two kinds of state machines are de?ned in UML:state machines and protocol state

1The normative text is the(formal)text de?ning the standard.In case of doubt it super-sedes all other explanations of the standard text.

5

machines.The semantics of state machines in the OMEGA kernel language is de?ned in[12].

We propose to use protocol state-machines as a visual formalism for speci-fying the set of all legal communication histories.The study of protocol state machines is outside the scope of this report.

1.2.3Sequence Diagrams

The UML sequence diagrams are replaced by life sequence charts in this project.

Live sequence charts are a suitable formalism for specifying liveness proper-ties of objects.Therefore we restrict ASO to the speci?cation of safety proper-ties.

1.2.4The Object Constraint Language

Our speci?cation language for architectural descriptions is based on OCL version 2.0[5].Event though we have identi?ed many inadequacies of OCL,we have decided to use a conservative extension of OCL.This means that most existing OCL constraints are still usable as ASO constraints.The concrete syntax of the language is the same whenever the semantics of the expressions are the same. Existing models may be converted to our formalism without any change and still have the same meaning.Some constraints will have a di?erent meaning in our language,because we have decided to use a two-valued interpretation of constraints.In these cases we changed the syntax,to make the di?erences apparent.

OCL was not designed to be a speci?cation language,and it does not work well as a constraint language.Di?erent design decisions during the development of OCL make it closer to a query language like SQL and OQL[10,35].

Chapter2discusses the problems we have identi?ed in OCL and how we in-tend to?x them.Chapter4de?nes the abstract syntax of our assertion language and points out the syntactic di?erences.Chapter5describes the semantics of ASO and summarises the semantic di?erences of our assertion language.

1.3Design Aims

The language we propose is designed to achieve the following goals:

?The assertion language de?ned in this report should not interfere with the many UML-based design methods.Instead,we want to de?ne a precise speci?cation language,which can be integrated seamlessly into these de-sign methods.Hence,we have to take the following methods into account:

–Abstraction and re?nement are used in many UML-based methods.

Very often a class is re?ned into a collection of classes;then an object

may be re?ned into a collection of objects.See for instance[14].

–Aspect orientation:Systems are commonly modelled by a collection of diagrams,depending on the desired functionality.We do not be-

lieve that someone will describe an implementation of a CORBA com-

ponent written in Java with an UML diagram,because a vast num-

ber of classes and methods are involved only to access the CORBA

6

services.Instead,a collection of class diagrams is used to describe

di?erent aspects of these classes.As a consequence,we have to take

into account,that a class diagram may lack information which may

appear in the implementation.

?UML Class Diagrams are not well suited to describe the dynamic object structures of object-oriented programs.Object diagrams,a kind of class diagrams,can be used to illustrate snapshots of object structures.Hence,

a formula will be evaluated in the context of an object structure.

?The language should support operational speci?cations in the style of Eif-fel[26,27].Each class is equipped with an invariant Each method is described in terms of pre-and postconditions.These are two predicates relating initial states of a method call to its?nal states.

?A history mechanism is de?ned,with a language to reason about histories.

Our speci?cations are split into two levels.The local speci?cation language is used to de?ne properties of the local state of an object.The local state of an object is given by the valuation of all its instance variables and the valuation of a methods parameters.On the local level it is not possible to dereference the state of other objects.The global speci?cation language is used to do this.It is used to specify properties of the object structure.

ASO di?ers from OCL in the following ways:

?ASO is an assertion language for object structures.Our assertions are intended to describe properties of object structures.This is a subset of the intended functionality of OCL2.0.

?OCL as published in[30]does not have a clear formal semantics.The situation is changing in OCL2.0,where a formal semantics for OCL is currently being developed.We do not want to wait for the completion of this task.

?OCL does not distinguish between local and global speci?cations.The distinction between a local and a global assertion language adheres to the principle of information hiding and supports a compositional description of the behaviour of a system of objects.Also,the lack of this distinction can be used to violate the information hiding principle:It is possible to de?ne class invariants,which make assumptions about the state of other objects using the navigation mechanism.As a result,we can give implementations, where a local change of an object violate the class invariant of another object.An example is given in[3].

?OCL is a three-valued logic.This is not adequate for an assertion language: What exactly is the meaning of a state formula,whose value is unde?ned?

Our assertion language is two-valued,but it contains special artifacts for unde?ned values of expressions only.No boolean expression will have an unde?ned value.

7

1.4The Semantic Model

Part of the speci?cation of the system are assertions.Another part of it are UML class diagrams,which give a structural description of a system.The structural description comprises the instance variables,methods,and typing information. The class diagram also conveys other safety properties,which will be explained in Chapter3.1.3.

?A class diagram does not specify behavioural aspects of an instance of any class appearing in it.

?Many structural aspects of object structures cannot be speci?ed in class diagrams alone.A logical formalism has to be used to de?ne constraints on object structures.

Object structures are the fundamental semantic entities of this report.Ob-ject structures will be formalised and discussed in Section3.1.4.

1.5Roadmap

In Chapter2we collect the problems of the syntax and semantics we have found with OCL.We motivate what needs to be changed,and why it has to be changed.This will motivate a language di?erent from OCL.

Chapter3contains a description of a typed logic with subtypes.This logic is the formal foundation of our assertion language for object structures.We describe the mathematical notation used in this report,de?ne the type system of the logic,describe the formal syntax and semantics of the logic,and relate it to object structures.

Chapter4de?nes the abstract syntax of the assertion language.The scope of this chapter is similar to the OCL“meta model.”Instead of expressing the “meta model”in UML we use conventional abstract grammar.We do not de?ne the di?erent levels of assertions within the abstract syntax.Only the means to declare the intended level of assertions or expressions are provided.Chapter5 describes the formal semantics of the assertion language de?ned in Chapter4.

Chapter6describes the formal semantics of the data types which we as-sume to be present in the assertion language.Here we introduce the formal semantics of the data types commonly used in programming languages,de?ne collection types like sets,bags,and sequences,and de?ne histories of communi-cation events.

Chapter7describes the pragmatics of using our assertion language and gives an example on how to specify with ASO.Chapter8gives a?nal conclusion and describes future work.

Appendix A de?nes the concrete syntax of our assertion language in BNF. We also de?ne the interchange formats of constraint language.

We have tried to provide a comprehensive index for this report.If a page reference is set in bold face,then it refers to the de?nition of the entry.Page references set in Roman font point to instructive examples.

Furthermore,we used the following typographic conventions:Names of mod-elling entities appearing in the UML Standard Document are written in Sans Serif type https://www.wendangku.net/doc/1818064098.html,s de?ned in the concrete syntax of the assertion language

8

are written in tele type type https://www.wendangku.net/doc/1818064098.html,s de?ned in the semantic domain of each of these languages are written in italic type face. Acknowledgements

Willem-Paul de Roever has commented on many versions of this report and gave valuable hints on references used in this report.

Martin Ste?en has helped to clarify many items of this report and was always available for discussions.

9

Chapter2

OCL Issues

This chapter describes the problems we have with the Object Constraint Lan-guage(OCL)and why we need a di?erent speci?cation language.OCL is not perfect.Indeed,many issues have been identi?ed in the OCL,see for exam-ple[38,10,36,6].We list the most prominent issues,which are neither changed in[5]nor in[35],which is the basis for Appendix A of[5].

These issues were essentially the result of a series of design decisions.These decisions made OCL unsuitable for formal speci?cation and veri?cation.These design decisions also invalidated some of the design aims of OCL.According to[10]OCL’s most important features are:

?Tight integration with the UML notation

?Pure speci?cation language without operational semantics

?Basic types like Boolean,Integer,Float

?Container types Collection,Bag,Sequence,and Sets with ap-

propriate operators

?The full type system also includes the types induced by class

de?nitions within UML

?Navigation expressions to navigate along associations with var-

ious multiplicities

?Boolean operators to allow full propositional logic

?Existential and universal quanti?ers over existing sets of objects

?Speci?cations are(to a large extend)executable and can there-

fore be used as assertions when animating the UML diagrams

or generating code

OCL is a speci?cation language that tries to mediate between the

practical users needs and the theoretical work that has been done in

that area.

Our discussion of OCL starts with a short critique of OCL’s type system.

2.1Type System

OCL’s type system is de?ned on top of UML’s type system[5,2].Types in OCL are indeed classes of object oriented programming languages.Because of this,

10

many speci?cations which make sense from a mathematical point of view are invalid in OCL;and algebraic laws do not hold anymore.To have a checkable type system,the speci?er has to frequently use explicit type coercions.This leads to some usability issues.

2.1.1Object-Oriented Type System

First,the type system of OCL is based on type systems of object-oriented pro-gramming languages.This results in some annoying restrictions.Among others, the union operation on sets is not commutative anymore.

Example2.1.1.The expression3.0+4is well typed,but4+3.0is not.

This example mainly breaks,because the type Integer is a subtype of Real, and both classes de?ne an operation+with signature Integer×Integer→Integer and Real×Real→Real,but does not decide which one to use.The inheritance of UML on the other hand,mandates that the latter signature has to be taken. Example2.1.2.Ifθ1 θ2and s1is of typeθ1and s2is of typeθ2,then the expression s2.union(s1)is well de?ned and returns a collection of type Set[θ2], but s1.union(s2)is not well typed,because Set[θ1] Set[θ2]and the result would be of type Set[θ2].

This basically means that many operations lose their algebraic properties. We may conclude,that s2.union(s1)=s1.union(s2).

2.1.2Navigation and Types

Navigating an association with multiplicity zero or one results in an object with two types:The type of the object at the association end and a(singleton)set of this type.The use of the accessor operators(.or->)decides which type is used.However,using strong typing becomes di?cult in this setting.

Example 2.1.3.If manager is an association with multiplicity zero or one to an object of type Manager,then the expression self.manager is an object of type Manager.Writing self.manager->size()coerces this object to the type Set(Manager).

2.1.3Parameterisation

UML provides the linguistic means to de?ne parameterised classes and depen-dent types.But the formal semantics are not de?ned for these entities.Espe-cially,there are no rules de?ned which relate these concepts with generalisation.

OCL uses parameterised classes too,and de?nes a type system for these. However,it does not generalise to the classes of a UML diagram.

OCL does not allow bounded parameterisation,which makes many con-straints overly verbose.

Example2.1.4.Instead of declaring a type with s:Set(T<:Ordered)to assert that all elements of the set can be ordered,one has to write constraints like

s->forall(e|e.oclIsType(Ordered)and?(e))

to make use of this property.

11

2.1.4Inheritance

The OCL standard by itself does not de?ne how to constraints and sub-classing work together.

The UML standard mandates,that a subclass has to satisfy the union of all constraints de?ned in its super-classes(see[30,p.2-70]):

The constraints on the full descriptor ore the union of the constraints

on the segment itself and all of its ancestors.If any of them are

inconsistent then the model is ill formed.

This restricts sub-classing to(behavioural)sub-typing.Software developers often use sub-classing and overriding to change the behaviour of classes.

2.1.5Access Modi?ers

OCL does not take access modi?ers like private,protected,and public into ac-count.Constraints are written in a way that all features of a class are considered to be public.This is not a real problem.But the speci?er has to exercise extra discipline,if his speci?cations are to be useful for clients of an API.

2.2Semantics

OCL allows the use of operations in speci?cations.This may lead to the follow-ing problems:

?It adds to the operational?avor of OCL.The execution of an operation may be nonterminating or result in unde?ned.In these cases the expres-sion containing this operation is said to be unde?ned.It is in general undecidable,whether such an operation is nonterminating,which adds to the complexity of the assertion language.

?Consider an operation applied to a collection of objects that are instances of some class C.Some elements of the collection may be of instances of one of C s subclasses,say D.If D rede?nes this operation,it is not de?ned which operation has to be applied to each object of the collection.Even if we assume“late-binding”,the meaning of all constraints may change during the evolution of the model,just by adding new subclasses which override the method used.

By this mechanism,it is even possible to invalidate constraints in a model, in that a subclass introduces a side-e?ect into the operation used for a speci?cation.

2.2.1Ill-de?ned Three Valued Logic

OCL is a three-valued logic,which adds a truth-value“unde?ned”to the tra-ditional truth values“true”and“false”.More importantly,OCL allows any expression to have an unde?ned value.However,the standard does not give a hint on what the meaning of such an unde?ned constraint is.This creates some pitfalls for the modeller.

12

If OCL is used as an assertion,the standard silently assumes,that the result of an OCL expression is either true or false.In Chapter7of the OCL2.0 submission version1.5,it is only de?ned,when an invariant,precondition,and postcondition has to hold.Otherwise the model is considered to be“ill-formed”. By this,we can conclude,that if a constraint is unde?ned when used as an invariant,precondition,or postcondition,then the diagram is ill-formed.

OCL expression may also appear as the initial value of an attribute or as a guard in a state machine.In these cases,the value needs an explanation. The standard o?ers no interpretation for this value.We introduce two possible explanations:

Exceptional Termination1The evaluation of the expression would raise an exception or return an arbitrary value.Examples of such situations are dereferencing a NULL pointer and division by zero.If the evaluation of the expression results in a method invocation,whose precondition or postcondition are violated by the parameter values,then we may also encounter an exception.

Divergence The evaluation of the constraint does not terminate,but results in an in?nite computation.One example of such an expression would be

a query operation resulting in the execution of an in?nite loop.

This also means,that in addition to?rst and?nal states,we also need a state modelling non-termination.We de?ne non-termination as divergence,that is,the computation does not terminate,and abnormal termination,that is,the computation aborts with an exception.We usually say,that the value of a non-terminating computation is unde?ned.Conversely,this should be the sole purpose of unde?ned.

A three-valued logic is mainly useful if you want to reason about total cor-rectness of programs.In contrast to partial correctness,we call a program totally correct,if it satis?es its speci?cation and,if the precondition is satis?ed, is guaranteed to terminate.

The formal semantics of OCL is based on a three-valued logic with strict se-mantics.Essentially,a three-valued logic usable for program veri?cation should satisfy the following conditions:

1.It de?nes negation as a monotone function on the?at cpo

B⊥def={true,false,⊥B},(2.1) and conjunction,disjunction,and implication as monotone functions from B⊥×B⊥→B⊥.Restricting these functions to B×B→B gives the

classical logical connectives.

2.The conjunction∧satis?es the equation

[[false∧undef]]=[[undef∧false]]=false,(2.2) and by this also

[[true∨undef]]=[[undef∨true]]=true.(2.3) 1This is sometimes called abnormal termination.

13

3.Existential quanti?cation should be equivalent to disjunction,and uni-

versal quanti?cation should be equivalent to conjunction.By this,the

reasonable predicate

?x.1

x

=1(2.4)

is equivalent to

x 1

x

=1(2.5)

and denotes true instead of⊥B,as a strict semantics would require. These conditions are met by Kleene’s logic[21],and the conditions?rst two conditions are re?ected in the de?nition of standard OCL.Table2.1summarises the semantics of boolean connectives satisfying conditions1and2.

a b not a a and b a or b a implies b

false false true false false true

false true true false true true

false⊥B true false⊥B true

true false false false true false

true true false true true true

true⊥B false⊥B true⊥B

⊥B false⊥B false⊥B⊥B

⊥B true⊥B⊥B true true

⊥B⊥B⊥B⊥B⊥B⊥B

Table2.1:Semantics of OCL’s Boolean Connectives

One unfortunate fact on OCL is,that it mixes the truth value of a constraint with the fact whether the constraints de?nition is computable or not by a cer-tain interpreter.This will impose many challenges for implementers.Consider formula(2.4),which may be written as

Integer.allInstances()->exists(x|1/x=1)

in OCL.Because the expression Integer.allInstances()does not denote a ?nite set,the value of the constraint is unde?ned,even though a satisfying value for x can be found by symbolic,algebraic rewriting of the constraint.This also demonstrates that OCL does not satisfy condition3.

Example2.2.1.Both expressions?i:i∈{0,1}→i

i =1is unde?ned,as is the

negation?i:i∈{0,1}∧i

i

=1.

The OCL standard mandates that each non-terminating operation call re-turns the value unde?ned.This is in general not decidable,which makes it impossible for tool vendors to implement the semantics of OCL(see also Sec-tion2.2.6).In combination with the strict evaluation strategy,all statements over in?nite sets are unde?ned.

Example 2.2.2.In OCL,the tautology?i.i∈I→i=i is unde?ned for all in?nite sets I.

At last,the presence of unde?ned constraints and their use raises the question what it means to satisfy unde?ned.This is not answered.

14

Example2.2.3.Obviously,any terminating program implements the post-condition ?i.i∈I→i=i,but this constraint is unde?ned.

Within the theory we have described here,we will show that the following formula does not have a meaning in our three valued logic:

?x(1

x

=1→x=1)(2.6)

By propositional reasoning and condition3we can convert the formula to

x (

1

x

=1∨x=1)

for which the term1

x =1∨x=1is true if x=0and unde?ned for x=0.

Hence the interpretation of(2.6)is⊥B∧true,which is unde?ned.

The solution to this problem is to de?ne equality as strong equality.

2.2.2Equality

OCL does not de?ne the notion of equality to use.2If one writes a=b,it is not clear how to interpret this constraint.We have the following choices:?a and b are of the same type and all their attribute values are equal.This is called structural equality.

?a and b are identi?ed by the same unique object identi?er.This is called reference equality.

Additionally,we have to choose how we will handle unde?ned.Again we may choose between:

?Strong equality,where⊥=⊥is true.

?Weak equality,where⊥=⊥is unde?ned.

The OCL2.0standard only decides the latter question,while the?rst question is still open.

Strong equality is de?ned as:

[[x=y]]=

true if[[x]]=[[y]].

false otherwise.

(2.7)

By this we have[[⊥B=⊥B]]=true and[[⊥B=1]]=false.

We strongly believe that a good assertion language possesses at least a strong equality operator;it allows us to conveniently solve the above problem,and also provides the most precise notion of equality of which all others can be de?ned. Remark 2.2.4.If you introduce strong relations,in which[[R ⊥B]]=false holds,the logic becomes a two valued?rst-order logic.This can be extended to a class logic,either by following Oberschelp,or by introducing the axioms of Zermelo and Fraenkel.

Additionally,equality is de?ned as an operation on OclAny,and it does not exclude the possibility of overriding this operation.

Example2.2.5.Assume that class C overrides=to mean equality on all at-tributes except one,say a.Then it is not guaranteed,that a=b implies a.a=b.a.

2In[10]an answer to this question is proposed.

15

2.2.3Fix-point Semantics

OCL allows the de?nition of recursive predicates and functions,but their?x-point semantics is not precisely de?ned[30,p.6-13]:

The right-hand-side of this de?nition may refer to the operation

being de?ned:that is,the de?nition may be recursive as long as the

recursion is not in?nite.

In general it is not decidable whether a recursive is in?nite.Also,the meaning of such an expression is only de?ned if the recursion is not in?nite.

Example2.2.6.Consider the speci?cation:

context number.M(n:Integer):Integer

pre:n=self.M(n)

post:result=self.M(n)

What is the interpretation of this speci?cation?Is M the unde?ned function? Or is this speci?cation illegal?Or is M denoting the identity function?And under which conditions may M be called?

This mixes declarative semantics,which were a design goal of OCL,with operational semantics.Also,it is not decidable,whether a?x-point can be reached in a?nite number of iteration steps,but sometimes a?x-point can be deduced without knowing the number of iteration steps.Such a solution must not be used,unless one has proven that the number of steps to reach this ?x-point is?nite.

Such a requirement is to be too strong for a speci?cation language.

2.2.4Flattening

Due to the?attening in OCL there is no distinction between non-deterministic functions and function returning sets.A non-deterministic function returning sets has the same signature as a deterministic function returning a set:both return set.

OCL de?nes the semantic convention that each set containing an unde?ned value has to be unde?ned.As a consequence,the following statements are all true:

⊥∈{⊥}

{⊥,X}={⊥,Y}

head(X,⊥)=⊥

The?attening operations are not worked out well.In OCL1.4it is not speci?ed,how to?atten({1,2,3},{3,4,5}).Only the explicit?attening mecha-nisms of OCL2.0give the user some control over these operations by providing an orderedBy operation converting sets to sequences.

2.2.5The Meaning of@pre

OCL does not de?ne an exact meaning of the@pre post?x-operator.The in-tended meaning is the value of an attribute,variable,or method in the preceding

16

国际贸易实务复习资料

国际贸易实务复习资料 一、名词解释 1、对等样:在实际业务中,如果卖方认为按买方来样供货没有切实把握,卖方可以根据买方来样仿制或从现有货物中选择品质相近的样品提供给买方。这种样品称为对等样品或回样。 2、航次租船:定程租船(voyage charter),又称航次租船,指船泊所有人负责提供船泊,在指定港口之间进行一个航次或数个航次,承运指定货物的租船运输。分单程,来回航次,连续航次,包运合同。 3、远期付款交单:(D/P after sight)系由出口人通过银行向进口人提示汇票和货运单据,进口人即在汇票上承兑,并于汇票到期日由代收银行再次向其提示时经付款后向代收银行取得单据。在汇票到期付款前,汇票和货运单据由代收行掌握。 4、品质公差:工业制成品在加工过程中所产生的误差,这种误差的存在是绝对的,其大小是由科技发展程度所决定的,是国际上公认的产品品质的误差。分国际、同行业公认的品质公差、交易双方公认的品质公差。 5、来料加工与进料加工:@来料加工在我国又称做对外加工装配业务,广义的来料加工包括来料加工和来件装配两个方面,是指由外商提供一定的原材料、零部件、元器件,由我方按对方的要求进行加工或装配,成品交由对方处置,我方按照约定收取工缴费作为报酬。@进料加工一般是指从国外购进原料,加工生产出成品再销往国外,由于进料加工的目的是扶持出口,所以进料加工也称“以进养出”。 6、预借提单:因信用证规定装运期和结汇期到期而货物因故未能及时装船,但已在承运人掌握之下或已开始装船,由托运人出具保函要求承运人预借的提单。 7、推定全损:推定全损是指该批被保险货物受损后,实际全损已经不可避免,或者恢复受损货物并将其送到保险单所注明的目的地所需要的费用将超过货物的价值。 8、实盘:指发盘一般要通过具体内容表示出发盘人(offeror)有肯定达成交易的意向,一旦受盘人(offeree)在有效期内无条件地接受发盘中的交易条件,交易即告达成,合同即告成立,双方均要受合同的约束。 9、汇票:汇票是一个人向另一个人签发的无条件的书面命令,要求接受命令的人在见票时或在指定的或可以确定的将来某一日期,支付一定的金额给特定的人或其指定的人或持有人。汇票是最主要的支付工具。 10、表提:表提,也称表盖提出,指议付行同意凭保议付后,在有关单据的表盖上标明“不符点”的内容,并注明“凭保议付”,然后将单据寄给开证行索汇。 11、收妥结汇:又称收妥付款,是指信用证议付行收到出口企业的出口单据后,经审查无误,将单据寄交国外付款行索取货款的结汇做法。这种方式下,议付行待收到付款行的货款后,即从国外付款行收到该行帐户的贷记通知书(credit note)时,才按当日外汇牌价,按照出口企业的指示,将货款折成人民币拨入出口企业的帐户。 12、CFR:“成本加运费”是指卖方在船上交货或以取得已经这样交付的货物方式交货。货物灭失或损坏的风险在货物交到船上时转移。卖方必须签订合同,并支付必要的成本和运费,将货物运至指定的目的港。

外贸提单样本BL draft

Shipper WUJIANG NEW LIGHT GARDEN FURNITURE CO.,LTD.SOUTH WUYUE ROAD,QIDU,WUJIANG,No.SHA11S0900972MULTIMODAL TRANSPORT BILL OF LADING Consignee ADW ECOMMERCE,LLC C/O PFLUG 17500 SHIDELER PARKWAY LATHROP,CA 95330 UNITED STATES Notify Party ADW ECOMMERCE,LLC C/O PFLUG 17500 SHIDELER PARKWAY LATHROP,CA 95330 UNITED STATES Place of receipt SHANGHAI Vessel Port of loading SHANGHAI ITAL UNIVERSO V.0329-063E Port of discharge Place of delivery OAKLAND Marks and numbers Numbers and kind of package Description of goods Gross weight Measurement according to the declaration of the shipper The contract evidenced by Bill of Lading is governed by the laws of Hong Kong Sepcial Administrative Region. Any proceedings aginst the Carrier must be brought in the courts of the Hong Kong Special Administrative Region and no other court. The goods and instructions are accepted and dealt with subject to the terms of this bill of lading including those on the back page. Taken in charge in apparent good order and condition, unless otherwise noted herein, at the place of eceipt for transport and delivery as mentioned above. If required by the Carrier, one original of these Multimodal Transport Bills of Lading must be surrendered duty endorsed in exchange for the goods. In Witness Whereof the original Multimodal Transport Bills of Lading of this tenor and date have been signed in the number stated below, one of which being accopmplished the other(s) to be void. Excess value declaration as per Clause 11.4 Freight amount Freight payable at Cargo Insurance through the undersigned Number of Original BL's Place and date of issue Stamp and signature For delivery of goods please apply to:DESTINATION AS THE CARRIER:not covered covered according to attached policy ALL FREIGHT INTERNATIONAL 131 S.W. 156TH ST SUITE 200SEATTLE, WA 98166 USA CY/DOOR SHIPPER'S LOAD & COUNT & SEAL 402CTN(S) 11306.00KGS 145.500CBM DESCRIPTION: GARDEN FURNITURE PO.#: Q'TY/CTN: DIMENSIONS:G.W/N.W.: MADE IN CHINA CONTAINER NO. /SEAL NO. /SIZE / NO. OF PKG/ GROSS WEIGHT/ MEAS. INBU3940013 /EMCCRM7578 /20'GP/ 63CTN(S)/ 1638.00KGS/ 29.400CBM EISU1628305 /EMCDTF8538 /40'GP/ 131CTN(S)/ 3406.00KGS/ 61.200CBM TGHU4818970 /EMCDTF9818 /40'GP/ 208CTN(S)/ 6262.00KGS/ 54.900CBM AS ARRANGE THREE(3) ON TIME EXPRESS LTD.(SHANGHAI)x SHANGHAI 06 APR 2009JIANGSU CHINA TEL:209 858 9170 TEL:209 858 9170 SHIPMENT ON BOARD DATE: 06 APR 2009 LATHROP FREIGHT COLLECT NON NEGOTIABLE COPY

国际贸易实务复习资料(整理版)

国际贸易实务复习提纲 第一章贸易术语 1.国际贸易术语的概念? 贸易术语,又称贸易条件、价格术语,是在长期的国际贸易实践中产生的,用来表明商品的价格构成,说明货物交接过程中的买卖双方有关风险、责任和费用的划分问题的专门术语。(如FOB) 2.与贸易术语有关的国际贸易惯例有哪些? 关于贸易术语的国际贸易惯例 《1932年华沙-牛津规则》——国际法协会,1928 《1941年美国对外贸易定义修订本》——美国九个商业团体,1919 《2010通则》——国际商会,1936 3.《2000通则》中FOB的主要内容及注意事项;CFR的内容及各种变形及与 CIF的区别、注意事项;CIF术语的注意事项?什么是到达合同? 1)《2000通则》中FOB的主要内容及注意事项: FOB(指定装运港),装运港船上交货 1、主要内容 ①买卖双方的义务 卖方: 将货装到船上(买方指定),或取得已如此交付的货物;承担交货前的费用和风险;办理出口手续;提供商业单据 买方: 支付价款;租船订舱并通知给卖方;承担交货后的费用和风险;办理 进口手续;受领货物并接受单据 2、注意事项 ①卖方代办租船订舱问题以及风险和费用的界定 ②船货的衔接问题 ③装货费用的负担问题(即FOB的变形问题) FOB班轮条件;FOB吊钩下交货;FOB包括理舱;FOB包括平舱 (注:该变形只是界定装货费用的负担问题,与风险的划分无关。) 2)CFR的内容及各种变形及与CIF的区别、注意事项 CFR (指定目的港),成本加运费 1、CFR的内容 买卖双方的义务 卖方: 将货装到船上(卖方指定)并通知买方,或取得已如此交付的货物;承 担交货前的费用和风险,但负担装运港到目的港的运费;租船或定舱;办理 出口手续;提供商业单据 买方: 支付价款;承担交货后的费用和风险(不包括从装运港到目的港的运费);办理进口手续;受领货物并接受单据 2、CFR各种变形

饥荒经典版 作弊码的运用与大全

饥荒控制台使用方法: 饥荒的控制台调出很简单,只要在游戏中按下“~”键(1左边的那个键)就可以调出游戏的控制台,如上图所示,这个界面下就可以输入相应的指令了。再按下回车就可以执行输入的指令。如上图所示,可能有的玩家会问屏幕中的那些字怎么去除,不然挡着游戏很难受,这里按下Ctrl+L就可以去除那些残留的字幕了! 饥荒作弊代码使用: 游戏中控制台可以输入作弊码 GetPlayer().components.builder:GiveAllRecipes() ---------- 全物品直接制造GetPlayer().components.hungerause(true) ---------- 饥饿值不降低 GetPlayer().components.sanity:SetMax(500) ---------- 精神值不降低(慎用不可取消)GetPlayer().components.health:SetMaxHealth(300) ---------- 最大血格 GetPlayer().components.health:SetInvincible(true) ---------- 上帝模式 下面是开全地图,要输入2个指令才行,每次都要回车执行: minimap = TheSim:FindFirstEntityWithTag("minimap") minimap.MiniMap:ShowArea(0,0,0, 10000) 注意事项: 游戏中可能有玩家存在作弊码不可用的情况,这是因为游戏的作弊模式被关闭了。 这时候在电脑的(X):\Documents and Settings\(用户名)\My Documents\Klei\DoNotStarve\ settings.ini中找到游戏的settings.ini(游戏设置)文件,用记事本的方式打开,把其中的ENABLECONSOLE选项(开启作弊器)中的“ENABLECONSOLE = false”修改为“ENABLECONSOLE = true”就可以了。DebugSpawn“cutgrass”(草) DebugSpawn“twigs”(树枝) DebugSpawn“log”(木头) DebugSpawn“charcoal”(木炭) DebugSpawn“ash”(灰) DebugSpawn“cutreeds”(采下的芦苇) DebugSpawn“lightbulb”(荧光果) DebugSpawn“petals”(花瓣) DebugSpawn“petals_evil”(噩梦花瓣) DebugSpawn“pinecone”(松果) DebugSpawn“foliage”(叶子) DebugSpawn“cutlichen”(摘下的苔藓) DebugSpawn“wormlight”(虫子果) DebugSpawn“lureplantbulb”(食人花种子) DebugSpawn“flint”(燧石) DebugSpawn“nitre”(硝石) DebugSpawn“redgem”(红宝石) DebugSpawn“bluegem”(蓝宝石) DebugSpawn“purplegem”(紫宝石) DebugSpawn“greengem”(绿宝石) DebugSpawn“orangegem”(橙宝石)

国际贸易实务-提单习题

SUBJECT TO THE TERMS AND CONDITIONS ON BACK

1.回答并分析下列条款: 某银行在审核单据时发现提单上有如下批注: Shippers load、count and seal ,Carriers not responsible for quality, quantity, packing, condition and/or nature of goods。 问:这是否构成不清洁提单? 2.依照所附海运提单(附表1),回答下列问题: (1)该提单应由谁首先背书? (2)作为收货人的代理人,你如何知道找谁提货? (3)收货人提货时应交出几份提单? (4)收货人提货时是否应交出海运单? (5)卸货港是哪里? (6)谁是承运人? (7)该提单下有几个集装箱? (8)XYZ Co,Ltd是否一定是收货人? (9)提单是否一定要经过XYZ Co, Ltd背书 (10)该提单由谁签署? 1根据国际航运工会规定,下面三项内容批注不能视为提单不清洁:(1)不明确表示货物或包装不能令人满意,(2)强调承运人对于货物或包装性质引起的风险不负责任(3)否认承运人知悉货物的内容,重量,容积或技术规格。 因为Shippers load、count and seal ,Carriers not responsible for quality, quantity, packing, condition and/or nature of goods。均符合清洁提单,所以不能构成不清洁提单。 2(1)shanghai knitwear import&export corporation背书 (2)因为这份提单是只是提单,所以在Notify address里面找到提货人的信息,包括电话,地址。 (3)3份(4)应该(5)YOKOHAMA

各类外贸单据时间及填写大全

单据时间: 发票最早,汇票最晚,次晚是提单,其他的在中间 发票日期最早,一般是提单日期前7天,不可和提单日期相差过大,例如超过20天,汇票日期最晚,产地证等单据的日期都需早于提单日期 时间顺序 1.汇票:等于或晚于发票日期; 2.商业发票:一般可以先于或等于提单日期,也可以迟于提单日期,但是不能超过信用证规定的交单日期或合理的交单日期。 3.海关发票:不应迟于提单日期。 4.形式发票:先于装运日期。 5.领事发票:不应迟于汇票和提单日期。 6.提单:不得超过信用证规定装运期,不能早于最早装运期。 7.保险单:投保日期除信用证有特殊规定外,应先于或等于提单日期,如果日期在提单日期后,则要有信用证特别许可,并写名保险责任及何时生效。 8.装箱单、重量单:与发票日期相同或略迟于发票日期,不应早于发票日期。9.一般产地证书:可以迟于发票日期,但不能迟于提单日期。 10.普惠制产地证书:普惠制产地证书发票上的号码和日期必须按照正式商业发票填写,签证当局签署日期和出口商签署日期不得早于发票日期。 11.检验检疫证书:不能迟于提单日期,但某些鲜活产品不能过分早于提单日期。 12.出口许可证:先于或早于提单日期。 13.受益人证明:晚于或等于提单日期。 14.电报、电传或传真抄本:等于或晚于提单日期3天内。但信用证规定早的,要按信用证。 15.船长收据或证明:等于或晚于提单日期。 16.船公司船证明:早于或等于提单日期。 17.运费收据:早于或等于提单日期。 包装单据的内容、作用及种类 包装单据主要包括:装箱单、重量单、包装说明(PACKING LIST、WEIGHT LIST AND PACKING SPECIFICATION)等,是商业发票内容的补充,通过对商品的包装件数、规格、唛头、重量等项目的填制,明确阐明商品的包装情况,便于买方对进口商品包装及数量、重量等的了解和掌握,也便于国外买方在货物到达目的港时,供海关检查和核对货物。也有的商品不需要包装,如谷物、矿砂、煤炭等,称之为“散装货物”(PACKED IN BULK)。而大多数商品必须加以适当的包装后才能装运出口,以保护该商品的安全。(此处显示一张真实的装箱单)图十一、常用的包装单据有以下几种:1、装箱单(PACKING LISTA或 PACKING SLIP);2、重量单(WEIGHT LIST 或WIGHT NOTE);3、尺码单(MEASUREMENT LIST);4、详细装箱单(DETAILED PACKING 1

《饥荒:联机版》自制MOD教程

《饥荒:联机版》自制MOD教程 [pagesplitxx][pagetitle]准备工作[/pagetitle] 饥荒联机版中的MOD作为游戏中的一大特色,深受玩家喜爱,但是那么多MOD里面没有自己喜欢的MOD怎么办,自己可以制作MOD吗,怎么制作》今天小编为大家带来了关于玩家如何自建MOD的教程,不妨仔细看看。 准备工作: 编写MOD所需要的工具 编辑Lua文件时,推荐使用 notepad++,或者Vi/Vim(少数像我这样的人才会用的编辑器 )。 不过如果你是程序猿,也许更想使用专为Lua设计的IDE。 当你需要编辑材质文件(本游戏中要求的材质文件格式是 .tex),推荐使用由 Handsome Matt 制作的TexTool(请在Klei论坛登陆后下载,你可以使用Steam登陆) 当你需要编辑png文件时,请使用支持透明背景的图像编辑器;如果你有闲钱,不妨买 个Photoshop;如果你穷得响叮当,就只有试试GIMP这款免费软件。 最后推荐你从Steam下载一个Don't Starve Mod工具,操作步骤如下:

[pagesplitxx][pagetitle]MOD基本文件结构[/pagetitle] 更多相关资讯请关注:饥荒专题 MOD基本文件结构 这里我用由 Eyres1 制作的 Never Perish Icebox(永久保鲜羊大白勺冰箱)来作为例子: 如上图所示,一个必须具有两个文件: modmain.lua:游戏载入你制作的mod所需要的文件; modinfo.lua:储存mod的作者、版本等信息的文件。 接下来我们打开这两个文件看看: modinfo.lua 第一行描述了该mod的名称, --The name of the mod displayed in the 'mods' screen.

国际贸易实务

对一份转让信用证的翻译 ZZCNCMT35P03-2806-073690 * * AUTHENTICATION RESULT:CORRECT WITH CURRENCYKEY * * * -----------------INSTANCE TYPE AND TRANSMISSION------------------------------- ORIGINAL RECEIVED FROM SWIFT PRIORITY:NORMAL MASSAGE OUTPUT REFERENCE: 1820030813SCBLCNSXASHA1985279185 CORRESPONDENT INPUT REFERENCE:1820030813SCBLHKHHAXXX 3474073794 ——————————————MESSAGE HEADER—————————————— SWIFT OUTPUT:FIN 720 TRANSFER OF A DOC CREDIT 转让信用证 SENDER:SCBLHKHHXXX STANDARD CHARTERED BANK HONG KONG HK 发报行(转让行):渣打银行香港分行 RECEIVER:SCBLCNSXSHA STANDARD CHARTERED BANK(SHANGHAI BRANGH) SHANGHAI CN 收报行(通知行):渣打银行上海分行 MUR:GAMIMX 40B:FORM OF DOCUMENTARY CREDIT:IRREVOCABLE WITHOUT OUR CONFIRMATION 信用证类型:不可撤销(我行不保兑) 20:TRANSFERRING BANK’S REFER ENCE:149010476943-BT 转让行的参考号:149010476943-BT 21:DOCUMENTARY CREDIT NUMBER:M125602 原证号码:M125602 31C:DATE OF ISSUE:030803 开证日期:2003-08-03 31D:DATE AND PLACE OF EXPIRY:030911 AT RBOS HK COUNTERS 到期日期与地点:2003-09-11在苏格兰皇家银行香港分行柜台 52D:ISSUING BANK OF ORIG D/C –NM&ADDR:ROYAL BANK OF SCOTLAND PLC,L/C PROCESSING CENTRE,7/F STANDARD CHARTERED TOWER,388 KWUN TONG RD,KWUN TONG, KLN,H.K. 原证开证行:苏格兰皇家银行信用证中心(后面是地址)

海运提单的制作

3-1《海运提单的制作》 郑可立宁波外事学校 【课题】海运提单(高等教育出版社《外贸单证实务》第5章第2节第3小节) 【课时】1课时(45分钟) 【内容简析】 海运提单是货物的收据、物权的凭证,同时又是运输合同的证明,它是出口人凭以向银行办理结汇的主要单据之一,并且在运输业务的联系、费用的结算和对外索赔中都具有重要作用,因此正确掌握提单的缮制方法对进出口贸易的从业人员来说至关重要。 【学情简析】 职业高中的学生对理论的理解能力较弱,在实际中根据不同的情况灵活应用知识的能力更差,提单在外贸单证中属于较难的单据,为了让学生掌握正确的制作方法,需要在上课时加以引导,提高学生自主学习能力,充分发挥学生学习主体的作用。 学生对海运提单的性质、作用和分类应有所了解,并熟悉信用证的基本内容 【教学目标】 1、知识目标:掌握海运提单各栏目制作方法。 2、能力目标:根据信用证和相关资料能正确完成提单的缮制。 3、情感目标:通过填制海运提单培养学生工作中细致、务实的

职业精神 【重点难点】 重点:如何根据信用证和相关资料制作海运提单 难点:海运提单的收货人、被通知人和海运提单的签署 【教学方法及策略】 根据教学目标营造以人为本,以学生为中心的课堂氛围,实施教师精讲,学生多练的教学方式,对难点的训练通过启发引导,调动学生参与和自主学习的积极性,使职业高中学生能实现以教材为本的学习方式向以实践为本的学习方式转变。 【教学平台与资源】 多媒体 【教学过程】 教学步骤教学内容设计意图及目标达 成预测 1、 (约 3’)导 入1、要求学生回答提单的性质和作用, 然后展示几张运输单据的图片,让学生 回答哪一张是海运提单,并说明虽然不 同船公司使用的海运提单的格式和内 容有差异,但基本内容基本相同。 2、介绍本节课需要制作的空白海运提 单的格式 3、根据练习一分析信用证中常见的提 有利于加强学生对 海运提单的直观影 响,调动学生的学习 制作提单的积极性

《饥荒:联机版》四大建家福地解析 新手建家选址指南

《饥荒:联机版》四大建家福地解析新手建家选址指南[pagesplitxx][pagetitle]桦树林猪村[/pagetitle] 《饥荒:联机版》在哪里选址建家对游戏是有重大影响的,一个好的选址能够让游戏更顺利的进行,今天小编给大家带来四大建家福地解析,感兴趣的朋友一起来看看吧! 我将从四个部分指引大家如何一步步搭建起一座完美营地!今天带来的part1就是如何为你们的营地选址,主要分析几处适合建家的区域,通过资源分析、适合角色的推荐、地理位置的解析以及注意事项的提醒帮助你选出心仪的位置,使得大家的建家大业有一个良好的开端,感谢你的点击,期待你认真的看完,这些内容真的很赞! PS:老白开了很多素材档,切换不同的角色只为搜集更多的素材,不能保证百分百的全面,但我尽可能的给大家最详细的解析,而太细枝末节的和大众普遍知道的就不说了! 一号推荐地:桦树林猪村 推荐入住角色:火女薇洛、女武神薇格佛德、大力士沃尔夫冈

适宜理由:火女和女武神专属制造需要用到金块,此地方便随时用肉蛋与猪王兑换金块,开启万圣节可以额外获得猪王给予的糖果,兑换的糖果女武神也可以吃,食物丰富,特别是肉类,可以满足女武神与大力士的肚子。 不推荐居住此地的角色:蜘蛛人韦伯 理由无他,猪人对蜘蛛包括蜘蛛人韦伯有天然的仇恨,影响正常的游戏节奏。当然你可以拆了猪村,然后在黄昏后集中重建,外面围上围墙。

其他角色也都适宜居住此地,但是需要注意下面一点。 更多相关资讯请关注:饥荒:联机版专题 注意事项:不能随心所欲的砍伐桦树,桦树树精比松树树精雷夫要更加难以对付,特别是变身后失去穿着护甲能力的伍迪,桦树精召唤的坚果精和抽动的树根,都有很大的威胁,单独对抗一棵甚至更多的桦树精十分危险,即便单挑了一棵桦树精,也需要付出一定的代价。 (这货只能用斧头砍,普通角色12下,伍迪砍树有暴击只需6下斧击) 桦树精可以不断召唤50血量的坚果精儿子 是刷坚果和树枝的好办法,它的触手状根茎鞭击伤害为40,所以单独砍伐桦树精需要精确的走位和不断退后清理坚果精,当然也可以雇佣二师兄帮你一同砍伐,桦树精属于邪恶生物。 应对方法:1.及时种下坚果,减少桦树的仇恨值,避免成群桦树精出现;2.如果两棵以上桦树精连片出现,且你不打算对抗它们,远离此地区一段时间会自行消失(或者放火烧山,或者在树精面前疯狂种坚果消除仇恨);3.移植一定量的松树,来代替桦树的树木供给,而且松树树精更好控制和击杀。 资源分析:

小度写范文[国际贸易实务(含答案)]国际贸易实务辅导用书模板

[国际贸易实务(含答案)]国际贸易实务辅导用书 对外经济贸易大学远程教育学院 2006—2007学年第一学期 《国际贸易实务》课程 期末考试题型、复习范围、要求及复习方法 一、题型: 以客观知识题为主。主要是单项选择题、多项选择题和判断题。 二、复习范围: 章节顺序,请参与《国际贸易实务》教材 导论 第一章贸易术语与国际贸易惯例 第二章《2000通则》中的E 组、F 组和C 组贸易术语 第三章《2000通则》中的D 组贸易术语 第四章贸易术语的选用 第五章合同的标的物及其质量、数量与包装 三、复习要求: 导论要求 1.掌握国际贸易的特点 2.了解国际货物买卖使用的法律与惯例 3.了解本课程的研究的对象 4.了解国际货物买卖合同的主要条款 5.认真阅读本课程的学习方法 第一章要求: 1.认真阅读贸易术语的产生与发展。 2.认真阅读并知晓有关贸易术语的国际贸易惯例。 3.掌握国际贸易惯例的性质与作用。 第二章要求: 1.了解E 组贸易术语的主要特点 2.掌握F 组贸易术语的特点 3.重点掌握FCA 和FOB 贸易术语的特点及其注意的问题。 4.重点掌握C 组贸易术语中有关CIF 贸易术语的特点及其注意的问题 5.重点政务CIP 贸易术语的有关特点 第三章要求: 1.掌握D 组贸易术语的特点 2.重点掌握DES 贸易术语及其注意的问题。 第四章要求: 1.认真阅读本章的主要内容,并掌握不同贸易术语的不同特点 2.重点掌握常用贸易术语的变形及其涵义 3.重点掌握贸易术语与合同的关系。 4.重点掌握选用贸易术语时应该注意的问题。 第五章要求 1.掌握品名条款的主要内容 2.掌握品质的表示方法 3.掌握合同中如何规定商品的品质,及其方法。

国际贸易单证(商业发票、提单、装箱单等)样本

COMMERCIAL INVOICE
ISSUER XIAOGAN XINGFU TRADING CO., LTD. 8 YUQUAN ROAD, XIAOGAN, CHINA
商业发票 COMMERCIAL INVOICE
TO JUN CORPORATION. 76 SWERT STREET, SEOUL, KOREA NO. DATE
HK565656
TRANSPORT DETAILS FROM SHANGHAI,CHINA TO BUSAN,KOREA BY VESSEL S/C NO.
APRIL 15, 2010
L/C NO.
787878
ACD90875
TERMS OF PAYMENT IRREVOCABLE L/C AT 60 DAYS AFTER SIGHT QUANTITY UNIT PRICE AMOUNT
Marks and Numbers
Number and kind of package Description of goods
JUN SEOUL C/NO. 1-100
90000 PAIRS OF BABY’S COTTON SOCKS ART.NO: BCS 003 AT USD1.00/PAIR CIF 100 CARTONS BUSAN INCOTERM 2000 AS PER S/C NO.787878.
USD1.00/PAIR CIF BUSAN INCOTERM2000
USD 90,000.00
TOTAL: 90,000 PAIRS SAY TOTAL: SAY U.S. DOLLARS NINETY THOUSAND ONLY
USD 90,000.00
STATED ARE REMARKS:WE HEREBY STATED THAT THE DOODS ARE OF CHINESE ORIGIN AND ALL THE DATE TRUE ON THE INVOICE ARE TRUE AND CORRECT. BK9001 VESSEL: YIXIANG BK9001

《饥荒:联机版》金丝雀召唤悲剧毒

《饥荒:联机版》金丝雀召唤悲剧毒菇方法一览饥荒联机版游戏中,玩家可以利用金丝雀来召唤出悲剧毒菇,具体怎么操作呢?快来看今天小编为大家带来的饥荒联机版金丝雀召唤悲剧毒菇方法一览吧! 金丝雀召唤悲剧毒菇方法一览 将生病的金丝雀丢在毒菇蘑菇边上,金丝雀会随之爆炸死亡掉落1~3根羽毛。 然后,毒菇蘑菇会变成:原谅蘑菇!(划掉)悲剧蘑菇! 你再去砍这个悲剧蘑菇,悲剧毒菇就会召唤出来。

它的血量十分夸张,是目前最多血量的Boss!血量夸张的达到了99999!我没有开玩笑! 他会发射悲剧蘑菇炸弹!一个炸弹甚至可以造成175的血! 他还是和以前的毒菇一样会召唤增加自己护甲的蘑菇树,但,如果你不把这个当回事,你会后悔的。 更多相关资讯请关注:饥荒:联机版专题

当悲剧毒菇的所有蘑菇树都变为最大而且所有蘑菇树都存在的时候,它的护甲会夸张的上升到99%! 这简直是夸张的一个Boss,难度无法想象! 当你过了很久很久很久终于打完后,他的掉落物如下:

蛤蟆皮x2 任意色蘑菇x3~5 大肉x4~5 发光器蓝图,蘑菇灯蓝图,原谅帽色蘑菇帽蓝图,王祖蓝色蘑菇帽蓝图,中国红色蘑菇帽蓝图中的3个以及睡包蓝图! 你学习后能在"战斗"中找到它。 需要一个蛤蟆皮和一个生病的金丝雀制作,一做就是4个,虽然很不划算,用倒是很好用的

。 他可以装备手上后丢在一个地方形成一个睡包菌子区域,来使这个区域的所有的生物都睡大觉!(除玩家,不知道PVP有没有效果)。 这个睡包菌子区域可以存在18~20秒。 因为他可以它可以让生物睡觉,那么它就可以在你被追杀的时候救你一命。 当生物在这个区域内睡觉使,你攻击它(例攻击兔子),那么那个生物只会短暂逃跑或短暂揍你几下,然后继续睡觉,当你看到巨鹿在搞你家?一个睡包解决,当你看到蚁狮在你不打他的时候疯狂回血?一个睡包解决,当你看到龙蝇发怒准备放大招?一个睡包解决。 总体来说,悲剧蛤蟆是一个变T ai而又强大的生物,没有充足的经验和充足的装备请不要随意接近。 更多相关资讯请关注:饥荒:联机版专题

提单样本,多式联运提单样本怎么填写,样本提

提单样本,多式联运提单样本怎么填写,样本提单 国际贸易中,贸易双方需要彼此建立信任,才能继续合作下去。通过离岸公司来做国际贸易不仅能够节省流程和成本,而且客户也会给与更高的信任。确立合作以后就是交货和收获,这个过程中,会涉及到提单的问题。提单是指用以证明海航货物运输合同和货物已经由承运人接收或装船,以及承运人保证以交付货物的单证。通过中间一系列的操作,才能完成一单交易。如果是通过离岸公司的话,这个过程会简单一些。 提单样本 快递和空运是一回事吗?空运有提单快递有提单吗?客户怎么能拿到那个空运提单以便去提货呢? 国际快递同空运一样,是使用飞机运载物品,但二都有本质的不同,快递由专人负责收件,派件,属于绿色通道的无大的商业价值的货品,无提单,只是派件公司送货到给一个送货存根联方便核对物品而亦,而空运则需要货主委托进出口货运公司对货物数量,金额进行明确申报,过海关审核后,才可运送的有一定商业价值的,收发货主双方有汇款手续的,收款方需到税务交纳税费的货品,提货人需凭发货方寄出的提单,到海关或委托相应的货运公司办理进口清关手续后方可提货。 多式联运提单样本怎么填写 多式联运:由两种及其以上的交通工具相互衔接、转运而共同完成的运输过程统称为复合运输,我国习惯上称之为多式联运,并且其中必须有种方式是海运。 海陆联运也算是多式联运了,提单就是船公司出的,发货港就正常写,卸货港写海运部分能运到的最后一个港口,最终目的地写陆路运输要到达的内陆点或是内陆堆场的地方。 陆路部分如果是铁路,那一般都是运到目的地的堆场。陆路部分如果是公路,那一船都是会给运到门。其实这些是看那些船公司运输线路和规定。如果提单上有标明 CY/CY,那就是堆场到堆场了,如果是CY/SD 那就是堆场到门了。 样本提单 跟货代对完提单后,是不是就可以把这个副本传真给客人,让其付款?还是让货代另外出一个样本提单? 样本提单与正本提单有什么区别吗? 是不是就可以把这个副本传真给客人,让其付款?---一般来说不可以,因为这个提单是为了缮制正确,货代才和发货人相互核对一下,不具备物权凭证的作用。 还是让货代另外出一个样本提单? ----如果样本提单有误,双方更改之后,货代会再给一个更改后, 无误的提单(预审) 给发货人做最后的确认。 样本提单与正本提单有什么区别吗---区别太大了! 正本提单是物权凭证。在船开了以后,船公司或其授权的代理才能签发正式提单。样本提单只是预审性质的,就是在制单的阶段,为了防止提单描述有误,先打出一个样本,让发货人或者通过发货人给收货人先确认上面的描述是否正确。

饥荒联机版如何创建本地服务器 创建本地服务器步骤

饥荒联机版如何创建本地服务器创建本地服务器步骤怎么搭建本地服务器,想知道怎么搭建本地服务器的更多攻略及相关信息吗?下面小编就给大家详细解答一下,想要了解的玩家过来强势围观吧! 饥荒联机版如何创建本地服务器?下面小编为大家带来饥荒联机版本地服务器创建详解内容来自铁骨 1.首先选取游戏内的“Host Game”,作用是运行你创建的本地服务器! 2.一共有五个栏可以选择,“New Server”便是可以用来创建的新服务器。 选取其中任意一栏来在右侧的框内进行编辑。 【打码的部分是我用过的,默认是五个栏都是可以用的哦】 3.标签说明:

#Server Settings 可以在这里面修改你服务器最基本的设定 如名字(Name)、介绍(Description)、游戏模式(Game Mode)、玩家人数(Players)、服务器模式(Server Mode)、设置密码(Password)等各项。其中,游戏模式、服务器模式一旦生成了服务器将不可更换! Delete Server是删除服务器设置,会把你的服务器全部清空~包括各种设定~。 #World 调整服务器世界的各项设定,如资源/生物的数量! 每当你调节完毕后,可以通过下面的存盘按钮来把调节好的设定另存为,以便下次游戏使用。 一旦生成服务器后就不可更改啦!

#Mods 可以添加游戏模组,Server Mods为服务端mod,可以让玩家玩到你所安装的mod!Client Mods为客户端mod,只能创建者自己体验到,而其它玩家不能享受。 mod若被勾选则会启用,可随时更改。 #Rollback 用于回档,创建服务器时暂时用不着! #Bans 创建服务器暂时用不着,用来防熊孩子的。 就像拉黑名单一样的功能,方法应该是通过控制台。 【创建世界+他人加入】 1.一切设定完美了之后,点击“Resume World” 启动你的服务器! 2.耐心等待,即可加入自己创建的服务器。进入选人物界面。

国际贸易实务进出口贸易合同协议书样本

国际贸易实务进出口贸易合同协议书样本 文件编号TT-00-PPS-GGB-USP-UYY-0089

CONTRACT NO.: 26102 DATE: THE BUYERS: The ATS company ADDRESS :15th Road New York USA TEL:+0 FAX: 买方: 地址: THE SELLERS: ADDRESS:19th Chang An Road Xi’an shanngxi China TEL: FAX: 7 This Contract is made by and between the Buyers and the Sellers, whereby the Buyers agree to buy and the Sellers agree to sell the under mentioned commodity according to the terms and conditions stipulated below: 买方与卖方就以下条款达成协议:

1. COMMODITY: 2. COUNTRY AND MANUFACTURERS: 原产国及制造商:Made in China & LYZ Company 3. PACKING: To be packed in standard airway packing. The Sellers shall be liable for any damage of the commodity and expenses incurred on account of improper packing and for any rust attributable to inadequate or improper protective measures taken by the sellers in regard to the packing.

饥荒联机版新手入门攻略

饥荒联机版入门攻略 饥荒生存类游戏,玩法简单深受玩家喜爱。好多不喜欢游戏的女生都在尝试后喜欢上此游戏,有独特的彩蛋和奇遇。饥荒联机版出了有一段时间了,但是一直没有比较全面且系统的攻略。(此攻略适合刚开的世界,或后加入不想和其他人在一起的玩家) 基础操作篇 可鼠标单独操作,也可配合键盘进行游戏,推荐键盘鼠标配合(打BOSS和怪物走位方便)。W.A.S.D键操控角色上下左右。用鼠标与其他物品.生物.建筑互动。F键用于自动攻击,空格键用于自动采集。M键地图,TAB键玩家列表(单机TAB是地图)。Q键位逆时针旋转视角E键位反之。1234567890物品栏的快捷键(我都没用过都是用鼠标点)。鼠标左键移动或安置物品,右键将物品穿戴或物品互动。(有的mod物品有自己独特用法不一一叙述) 联机介绍篇 首先要先下载饥荒联机版,联机方法有很多Steam正版(请支持正版),游侠,蛤蟆吃等。 《饥荒Rev.173373》04.15可改名中文免安装绿色联机硬盘版 百度网盘:https://www.wendangku.net/doc/1818064098.html,/s/1nvxmwQX 旋风分享:https://www.wendangku.net/doc/1818064098.html,/?vmqMJjE 360云盘:https://https://www.wendangku.net/doc/1818064098.html,/cq4cyCheqDsXM 访问密码50e8 下载地址的部分转载至游侠官方帖子,原网站:https://www.wendangku.net/doc/1818064098.html,/thread-5544397-1-1.html 我以游侠为例(支持正版你还用游侠!)。下载完游侠和饥荒联机版后设置好路径。 路径设置例图:

这是开始界面: 一汉化游戏方法 从我这下载的游戏是英文的需要使用游戏带的mod改成中文方法如下: 1.开始界面点击Play! 会弹出一个对话框(这是Steam登录用的我们登录不上) 2.点击Play Offline(离线登录) 3.菜单页面点击Mods

外贸审核提单的要点

外贸审核提单的要点 一、整套正本提单注有张数。是否按信用证条款交呈。 二、提单正面是否打明承运人(CARRIER)的全名及“承运人(CARRIER)”一词以表明其身份。 三、如提单正面已作如上表示,在承运人自己签署提单时,签署处毋须再打明承运人一词及其全名。举例:如提单正面已打明(或印明)承运人全名为XYZ LINE及“CARRIER”一词以示明其身份,在提单签署处(一般在提单的右下角)经由XYZ LINE及其负责人签章即可。如提单正面未作如(二)表示;且由运输行(FORWARDER)签署提单时,则在签署处必须打明签署人的身份。如:ABC FORW ARDING CO as agents for XYZ LINE, the carrier或ABC FORW ARDING Co on behalf of XYZ LINE the carrier。如提单正面已作如(二)表示,但由运输行(FORWARDER)签署提单时,则在签署处必须打明签署人的身份,如ABC FORW ARDING CO as agents for the carrier或as agents for/on behalf of the carrier。 四、提单有印就“已装船”(“Shipped in apparent good order and condition on board…”)字样的,毋须加“装船批注”(“On board notation”);也有印就“收妥待运”(“Received in apparent good order and condition for shipment…”)字样的则必须再加“装船批注”并加上装船日期。 五、提单印有“intended vessel”、“intended port of loading”、“intended port of discharge”及/或其他“intended…”等不肯定的描述字样者,则必须加注“装船批注”,其中须把实际装货的船名,装货港口,卸货港口等项目打明,即使和预期(intended)的船名和装卸港口并无变动,也需重复打出。 六、单式海运即港对港(装货港到卸货港)运输方式下,只须在装货港(Port of Loading),海轮名(Ocean vessel),及卸货港(Port of Discharge)三栏内正确填写;如在中途转船(Transhipment),转船港(Port of tcano hipment)的港名,不能打在卸货港(Port of discharge)栏内。需要时,只可在提单的货物栏空间打明“在××(转船港)转船”“with transhipment at××”。 七、“港口”(Port)和“地点”(place)是不同的概念。有些提单印有“收货地点”(pla ce of receipt/taking in charge)和“交货地点/最后目的地”(place of delivery/final destination)等栏目,供提单用作“多式联运”(mulli-madal transport)或“联合运输”(combined transport)运输单据时用。单式海运时不能填注。否则会引起对运输方式究竟是单式海运抑或多式联运的误解。 八、提单上印有“前期运输由”(precarriage by)栏也为“多式联运”方式所专用,不能作为转船提单时打明第一程海轮名称的栏目。只有作多式联运运输单据时,方在该栏内注明“铁路”、“卡车”、“空运”或“江河”(Rail、truck、air、river)等运输方式。 九、提单的“收货人”栏(consigned to或consignee)须按信用证要求说明。例如,信用证规定提单作成“made out to order”,则打“order”一字;“made out to order of the applicant(申请开证

相关文档