当前位置：文档之家› Proving correctness of Timed Concurrent Constraint Programs

Proving correctness of Timed Concurrent Constraint Programs

a r

s /0

[

]

Proving correctness of Timed Concurrent Constraint Programs F.S.de Boer Universiteit Utrecht ?M.Gabbrielli Universit`a di Bologna §M.C.Meo Universit`a di Chieti ?Abstract A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs.The logic is based on modalities which allow one to specify what a process produces as a reaction to what its environment inputs.These modalities provide an assumption/commitment style of speci?cation which allows a sound and complete compositional axiomatization of the reactive behavior of timed concurrent constraint programs.Keywords :Concurrency,constraints,real-time programming,temporal logic.1Introduction Many “real-life”computer applications maintain some ongoing interaction with external physical pro-cesses and involve time-critical aspects.Characteristic of such applications,usually called real-time embedded systems,is the speci?cation of timing constraints such as,for example,that an input is re-quired within a bounded period of time.Typical examples of such systems are process controllers and signal processing systems.In [5]tccp ,a timed extension of the pure formalism of concurrent constraint programming([25]),is introduced.This extension is based on the hypothesis of bounded asynchrony (as introduced in [27]):Computation takes a bounded period of time rather than being instantaneous as in the concurrent synchronous languages ESTEREL [3],LUSTRE [16],SIGNAL [20]and Statecharts [17].Time itself is measured by a discrete global clock,i.e,the internal clock of the tccp process.In [5]we also introduced timed reactive sequences which describe at each moment in time the reaction of a tccp process to the input of the external environment.Formally,such a reaction is a pair of constraints c,d ,where c is the input given by the

environment and d is the constraint produced by the process in response to the input c (such a response includes always the input because of the monotonicity of ccp computations).

In this paper we introduce a temporal logic for describing and reasoning about timed reactive sequences.The basic assertions of the temporal logic describe the reactions of such a sequence in terms of modalities which express either what a process assumes about the inputs of the environment and what a process commits to,i.e.,has itself produced at one time-instant.These modalities thus provide a kind of as-sumption/commitment style of speci?cation of the reactive behavior of a process.The main result of this paper is a sound and complete compositional proof system for reasoning about the correctness of tccp programs as speci?ed by formulas in this temporal logic.

The remainder of this paper is organized as follows.In the next section we introduce the language tccp and its operational semantics.In Section 3we introduce the temporal logic and the compositional proof system.In Section 4we discuss soundness and completeness of the proof system.Section 5concludes by discussing related work and indicating future research.A preliminary,short version of this paper appeared in [7].

2The programming language

In this section we?rst de?ne the tccp language and then we de?ne formally its operational semantics by using a transition system.

Since the starting point is ccp,we introduce?rst some basic notions related to this programming paradigm.We refer to[26,28]for more details.The ccp languages are de?ned parametrically wrt to a given constraint system.The notion of constraint system has been formalized in[26]following Scott’s treatment of information systems.Here we only consider the resulting structure.

De?nition2.1A constraint system is a complete algebraic lattice C,≤,?,true,false where?is the lub operation,and true,false are the least and the greatest elements of C,respectively.

Following the standard terminology and notation,instead of≤we will refer to its inverse relation,denoted by?and called entailment.Formally,?c,d∈C.c?d?d≤c.In order to treat the hiding operator of the language a general notion of existential quanti?er is introduced which is formalized in terms of cylindric algebras[18].Moreover,in order to model parameter passing,diagonal elements[18]are added to the primitive constraints.This leads to the concept of a cylindric constraint system.In the following, we assume given a(denumerable)set of variables Var with typical elements x,y,z,....

De?nition2.2Let C,≤,?,true,false be a constraint system.Assume that for each x∈Var a function ?x:C→C is de?ned such that for any c,d∈C:

(i)c??x(c),(ii)if c?d then?x(c)??x(d),

(iii)?x(c??x(d))=?x(c)??x(d),(iv)?x(?y(c))=?y(?x(c)).

Moreover assume that for x,y ranging in Var,C contains the constraints d xy(so called diagonal elements) which satisfy the following axioms:

(v)true?d xx,(vi)if z=x,y then d xy=?z(d xz?d zy),

(vii)if x=y then d xy??x(c?d xy)?c.

Then C= C,≤,?,true,false,Var,?x,d xy is a cylindric constraint system.

Note that if C models the equality theory,then the elements d xy can be thought of as the formulas x=y. In the sequel we will identify a system C with its underlying set of constraints C and we will denote?x(c) by?x c with the convention that,in case of ambiguity,the scope of?x is limited to the?rst constraint sub-expression(so,for instance,?x c?d stands for?x(c)?d).

The basic idea underlying ccp is that computation progresses via monotonic accumulation of information in a global https://www.doczj.com/doc/5815017866.html,rmation is produced by the concurrent and asynchronous activity of several agents which can add(tell)a constraint to the store.Dually,agents can also check(ask)whether a constraint is entailed by the store,thus allowing synchronization among di?erent agents.Parallel composition in ccp is modeled by the interleaving of the basic actions of its components.

When querying the store for some information which is not present(yet)a ccp agent will simply suspend until the required information has arrived.In timed applications however often one cannot wait indef-initely for an event.Consider for example the case of a bank teller machine.Once a card is accepted and its identi?cation number has been checked,the machine asks the authorization of the bank to release the requested money.If the authorization does not arrive within a reasonable amount of time,then the card should be given back to the customer.A timed language should then allow us to specify that,in case a given time bound is exceeded(i.e.a time-out occurs),the wait is interrupted and an alternative action is taken.Moreover in some cases it is also necessary to abort an active process A and to start a process B when a speci?c event occurs(this is usually called preemption of A).For example,according to a typical pattern,A is the process controlling the normal activity of some physical device,the event indicates some abnormal situation and B is the exception handler.

In order to be able to specify these timing constraints in ccp we introduce a discrete global clock and assume that ask and tell actions take one https://www.doczj.com/doc/5815017866.html,putation evolves in steps of one time-unit, so called clock-cycles.We consider action pre?xing as the syntactic marker which distinguishes a time instant from the next one.Furthermore we make the assumption that parallel processes are executed on di?erent processors,which implies that at each moment every enabled agent of the system is activated. This assumption gives rise to what is called maximal parallelism.The time in between two successive moments of the global clock intuitively corresponds to the response time of the underlying constraint system.Thus essentially in our model all parallel agents are synchronized by the response time of the underlying constraint system.

Furthermore,on the basis of the above assumptions we introduce a timing construct of the form now c then A else B which can be interpreted as follows:If the constraint c is entailed by the store at the current time t then the above agent behaves as A at time t,otherwise it behaves as B at time t.As shown in[5,27]this basic construct allows one to derive such timing mechanisms as time-out and preemption. Thus we end up with the following syntax of timed concurrent constraint programming.

De?nition2.3[tccp Language[5]]Assuming a given cylindric constraint system C the syntax of agents is given by the following grammar:

A::=tell(c)| n i=1ask(c i)→A i|now c then A else B|A B|?xA|p(x)

where the c,c i are supposed to be?nite constraints(i.e.algebraic elements)in C.A tccp process P is then an object of the form D.A,where D is a set of procedure declarations of the form p(x)::A and A is an agent.

Action pre?xing is denoted by→,non-determinism is introduced via the guarded choice construct n i=1ask(c i)→A i,parallel composition is denoted by ,and a notion of locality is introduced by the agent?xA which behaves like A with x considered local to A,thus hiding the information on x pro-vided by the external environment.In the next subsection we describe formally the operational semantics of tccp.In order to simplify the notation,in the following we will omit the n i=1whenever n=1and we will use tell(c)→A as a shorthand for tell(c) (ask(true)→A).In the following we also assume guarded recursion,that is we assume that each procedure call is in the scope of an ask construct.This assumption,which does not limit the expressive power of the language,is needed to ensure a proper de?nition of the operational semantics.

2.1Operational semantics

The operational model of tccp can be formally described by a transition system T=(Conf,?→)where we assume that each transition step takes exactly one time-unit.Con?gurations(in)Conf are pairs consisting of a process and a constraint in C representing the common store.The transition relation ?→?Conf×Conf is the least relation satisfying the rules R1-R10in Table1and characterizes the (temporal)evolution of the system.So, A,c ?→ B,d means that if at time t we have the process A and the store c then at time t+1we have the process B and the store d.

Let us now brie?y discuss the rules in Table1.In order to represent successful termination we introduce the auxiliary agent stop:it cannot make any transition.Rule R1shows that we are considering here the so called“eventual”tell:The agent tell(c)adds c to the store d without checking for consistency of c?d and then stops.Note that the updated store c?d will be visible only starting from the next time instant since each transition step involves exactly one time-unit.According to rule R2the guarded choice operator gives rise to global non-determinism:The external environment can a?ect the choice since ask(c j)is enabled at time t(and A j is started at time t+1)i?the store d entails c j,and d can be modi?ed by other agents.The rules R3-R6show that the agent now c then A else B behaves as A or B depending on the fact that c is or is not entailed by the store.Di?erently from the case of the ask,here the evaluation of the guard is instantaneous:If A,d ( B,d )can make a transition at time t and c is(is not)entailed by the store d,then the agent now c then A else B can make the

R1 tell(c),d ?→ stop,c?d

R2 n i=1ask(c i)→A i,d ?→ A j,d j∈[1,n]and d?c j

A,d ?→ A′,d′

d?c

now c then A else B,d ?→ A,d

B,d ?→ B′,d′

d?c

now c then A else B,d ?→ B,d

A,c ?→ A′,c′ B,c ?→ B′,d′

A B,c ?→ A′ B,c′

B A,c ?→ B A′,c′

A,d??x c ?→ B,d′

p(x),c ?→ B,d p(x)::A∈D

Table1:The transition system for tccp.

same transition at time t.Moreover,observe that in any case the control is passed either to A(if c is entailed by the current store d)or to B(in case d does not entail c).Rules R7and R8model the parallel composition operator in terms of maximal parallelism:The agent A B executes in one time-unit all the initial enabled actions of A and B.Thus,for example,the agent A:(ask(c)→stop) (tell(c)→stop) evaluated in the store c will(successfully)terminate in one time-unit,while the same agent in the empty store will take two time-units to terminate.The agent?xA behaves like A,with x considered local to A,i.e.the information on x provided by the external environment is hidden to A and,conversely,the information on x produced locally by A is hidden to the external world.To describe locality in rule R9 the syntax has been extended by an agent?d xA where d is a local store of A containing information on x which is hidden in the external store.Initially the local store is empty,i.e.?xA=?true xA.

Rule R10treats the case of a procedure call when the actual parameter equals the formal parameter. We do not need more rules since,for the sake of simplicity,here and in the following we assume that the set D of procedure declarations is closed wrt parameter names:That is,for every procedure call p(y)appearing in a process D.A we assume that if the original declaration for p in D is p(x)::A then D contains also the declaration p(y)::?x(tell(d xy) A)1.

Using the transition system described by(the rules in)Table1we can now de?ne our notion of observables

which associates with an agent a set of timed reactive sequences of the form

c1,d1 ··· c n,d n d,d

where a pair of constraints c i,d i represents a reaction of the given agent at time i:Intuitively,the agent transforms the global store from c i to d i or,in other words,c i is the assumption on the external environment while d i is the contribution of the agent itself(which includes always the assumption).The last pair denotes a“stuttering step”in which no further information can be produced by the agent,thus indicating that a“resting point”has been reached.

Since the basic actions of tccp are monotonic and we can also model a new input of the external environ-ment by a corresponding tell operation,it is natural to assume that reactive sequences are monotonically increasing.So in the following we will assume that each timed reactive sequence c1,d1 ··· c n?1,d n?1 c n,c n satis?es the following condition:d i?c i and c j?d j?1,for any i∈[1,n?1]and j∈[2,n].Since the constraints arising from the reactions are?nite,we also assume that a reactive sequence contains only

?nite constraints2.

The set of all reactive sequences is denoted by S and its typical elements by s,s1...,while sets of reactive sequences are denoted by S,S1...andεindicates the empty reactive sequence.Furthermore,·denotes the operator which concatenates sequences.Operationally the reactive sequences of an agent are generated

as follows.

De?nition2.4We de?ne the semantics R∈Agent→P(S)by

R(A)={ c,d ·w∈S| A,c → B,d and w∈R(B)}

∪

{ c,c ·w∈S| A,c →and w∈R(A)∪{ε}}.

Note that R(A)is de?ned as the union of the set of all reactive sequences which start with a reaction of

A and the set of all reactive sequences which start with a stuttering step of A.In fact,when an agent is blocked,i.e.,it cannot react to the input of the environment,a stuttering step is generated.After such a stuttering step the computation can either continue with the further evaluation of A(possibly generating more stuttering steps)or it can terminate,as a“resting point”has been reached.These two case are

re?ected in the second part of the de?nition of R(A)by the two conditions w∈R(A)and w∈{ε}, respectively.Note also that,since the stop agent used in the transition system cannot make any move,

an arbitrary(?nite)sequence of stuttering steps is always appended to each reactive sequence.

Formally R is de?ned as the least?xed-point of the corresponding operatorΦ∈(Agent→P(S))→Agent→P(S)de?ned by

Φ(I)(A)={ c,d ·w∈S| A,c → B,d and w∈I(B)}

∪

{ c,c ·w∈S| A,c →and w∈I(A)∪{ε}}.

The ordering on Agent→P(S)is that of(point-wise extended)set-inclusion(it is straightforward to check thatΦis continuous).

3A calculus for tccp

In this section we introduce a temporal logic for reasoning about the reactive behavior of tccp programs. We?rst de?ne temporal formulas and the related notions of truth and validity in terms of timed reactive sequences.Then we introduce the correctness assertions that we consider and a corresponding proof system.

3.1Temporal logic

Given a set M,with typical element X,Y,...,of monadic constraint predicate variables,our temporal logic is based on atomic formulas of the form X(c),where c is a constraint of the given underlying constraint system.The distinguished predicate I will be used to express the“assumptions”of a process about its inputs,that is,I(c)holds if the process assumes the information represented by c is produced by its environment.On the other hand,the distinguished predicate O represents the output of a process, that is,O(c)holds if the information represented by c is produced by the process itself(recall that the produced information includes always the input,as previously mentioned).More precisely,these formulas I(c)and O(c)will be interpreted with respect to a reaction which consists of a pair of constraints c,d , where c represents the input of the external environment and d is the contribution of the process itself (as a reaction to the input c)which always contains c(i.e.such that d≥c holds).

An atomic formula in our temporal logic is a formula as described above or an atomic formula of the form c≤d which‘imports’information about the underlying constraint system,i.e.,c≤d holds if d?c. Compound formulas are constructed from these atomic formulas by using the(usual)logical operators of negation,conjunction and(existential)quanti?cation and the temporal operators (the next operator) and U(the until operator).We have the following three di?erent kinds of quanti?cation:?quanti?cation over the variables x,y,...of the underlying constraint system;

?quanti?cation over the constraints c,d,...themselves;

?quanti?cation over the monadic constraint predicate variables X,Y,....

Variables p,q,...will range over the constraints.We will use V,W,...,to denote a variable x of the underlying constraint system,a constraint variable p or a constraint predicate X.

De?nition3.1[Temporal formulas]Given an underlying constraint system with set of constraints C, formulas of the temporal logic are de?ned by

φ::=p≤q|X(c)|?φ|φ∧ψ|?Vφ| φ|φUψ

In the sequel we assume that the temporal operators have binding priority over the propositional con-nectives.We introduce the following abbreviations:c=d stands for c≤d∧d≤c,3φfor true Uφand 2φfor?3?φ.We also useφ∨ψas a shorthand for?(?φ∧?ψ)andφ→ψas a shorthand for?φ∨ψ. Finally,given a temporal formulaφ,we denote by F V(φ)(F V constr(φ))the set of the free(constraint)

variables ofφ.

De?nition3.2Given an underlying constraint system with set of constraints C,the truth of an atomic formula X(c)is de?ned with respect to a predicate assignment v∈M→C which assigns to each monadic predicate X a constraint.We de?ne

v|=X(c)if v(X)?c.

Thus X(c)holds if c is entailed by the constraint represented by X.In other words,a monadic constraint predicate X denotes a set{d|d?c}for some c.We restrict to constraint predicate assignments which are monotonic in the following sense:v(O)?v(I).In other words,the output of a process contains its input.

The temporal operators are interpreted with respect to?nite sequenceρ=v1,...,v n of constraint predicate assignments in the standard manner: φholds ifφholds in the next time-instant andφUψholds if there exists a future moment(possibly the present)in whichψholds and until thenφholds.We restrict to sequencesρ=v1,...,v n which are monotonic in the following sense:for1≤i

?v i+1(X)?v i(X),for every predicate X;

?v i+1(I)?v i(O).

The latter condition requires that the input of a process contains its output at the previous time-instant. Note that these conditions corresponds with the monotonicity of reactive sequences as de?ned above.

In order to de?ne the truth of a temporal formula we introduce the following notions:given a?nite sequenceρ=v1,...,v n of predicate assignments,we denote by l(ρ)=n the length ofρandρi=v i, 1≤i≤n.We also de?neρ<ρ′ifρis a proper su?x ofρ′(ρ≤ρ′ifρ<ρ′orρ=ρ′).Given a variable x of the underlying constraint systems and a predicate assignment v we de?ne the predicate assignment ?xv by?xv(X)=?x d,where d=v(X).Given a sequenceρ=v1,...,v n,we denote by?xρthe sequence ?xv1,...,?xv n.Moreover,given a monadic constraint predicate X and a predicate assignment v we denote by?Xv the restriction of v to M\{X}.Given a sequenceρ=v1,...,v n,we denote by?Xρthe sequence?Xv1,...,?Xv n.Furthermore,byγwe denote a constraint assignment which assigns to each constraint variable p a constraintγ(p).Finally,γ{c/p}denotes the result of assigning inγthe constraint c to the variable p.

Moreover,we assume that time does not stop,so actually a?nite sequence v1···v n represents the in?nite sequence v1···v n,v n,v n···with the last element repeated in?nitely many times.Formally,this assumption is re?ected in the following de?nition in the interpretation of the .By a slight abuse of notation,given a sequenceρ=v1···v n with n≥1we de?ne ρas follows

(n=1) v1=v1

(n>1) ρ=v2···v n.

The truth of a temporal formula is then de?ned as follows.

De?nition3.3Given a sequence of predicate assignmentsρ=v1,v2,...,v n,a constraint assignmentγandφa temporal formula,we de?neρ|=γφby:

by:

ρ|=γp≤q ifγ(q)?γ(p)

ρ|=γX(c)ifρ1|=X(c)

ρ|=γ?φifρ|=γφ

ρ|=γφ1∧φ2ifρ|=γφ1andρ|=γφ2

ρ|=γ?xφifρ′|=γφ,for someρ′s.t.?xρ=?xρ′

ρ|=γ?Xφifρ′|=γφ,for someρ′s.t.?Xρ=?Xρ′

ρ|=γ?pφifρ|=γ′φ,for some c s.t.γ′=γ{c/p}

ρ|=γ φif ρ|=γφ

ρ|=γφUψif for someρ′≤ρ,ρ′|=γψand for allρ′<ρ′′≤ρ,ρ′′|=γφ.

Moreoverρ|=φi?ρ|=γφfor every constraint assignmentγ.

De?nition3.4A formulaφis valid,notation|=φ,i?ρ|=φfor every sequenceρof predicate assign-ments.

We have the validity of the usual temporal tautologies.Monotonicity of the constraint predicates wrt the entailment relation of the underlying constraint system is expressed by the formula

?p?q?X(p≤q→(X(q)→X(p))).

Monotonicity of the constraint predicates wrt time implies the validity of the following formula

?p?X(X(p)→2X(p)).

The relation between the distinguished constraint predicates I and O is logically described by the laws

?p(I(p)→O(p))and?p(O(p)→ I(p)),

that is,the output of a process contains its input and is contained in the inputs of the next time-instant.

3.2The proof-system

We introduce now a proof-system for reasoning about the correctness of tccp programs.We?rst de?ne formally the correctness assertions and their validity.

De?nition3.5Correctness assertions are of the form A satφ,where A is a tccp process andφis a temporal formula.The validity of an assertion A satφ,denoted by|=A satφ,is de?ned as follows

|=A satφi?ρ|=φ,for allρ∈R′(A),

where

R′(A)={v1,...,v n| v1(I),v1(O) ··· v n(I),v n(O) ∈R(A)}.

Roughly,the correctness assertion A satφstates that every sequenceρof predicate assignments such that its‘projection’onto the distinguished predicates I and O generates a reactive sequence of A,satis?es the temporal formulaφ.

T1tell(c)sat O(c)∧?p(O(p)→?q(I(q)∧q?c=p))∧ 2stut

A i satφi,?i∈[1,n]

now c then A else B sat(I(c)∧φ)∨(?I(c)∧ψ)

T4A satφ

A B sat?X,Y(φ[X/O]∧ψ[Y/O]∧par(X,Y))X,Y∈F V(φ)∪F V(ψ),X=Y

p(x)satφ?p A satφ

A satψ

Table2:The system TL for tccp.

Table2presents the proof-system.

Axiom T1states that the execution of tell(c)consists of the output of c(as described by O(c))together with any possible input(as described by I(q)).Moreover,at every time-instant in the future no further output is generated,which is expressed by the formula

?p(O(p)?I(p)),

which we abbreviate by stut(since it represents stuttering steps).

In rule T2I i stands for I(c i).Given that A i satis?esφi,rule T2allows the derivation of the speci?cation forΣn i=1ask(c i)→A i,which expresses that either eventually c i is an input and,consequently,φi holds in the next time-instant(since the evaluation of the ask takes one time-unit),or none of the guards is ever satis?ed.

Rule T3simply states that if A satis?esφand B satis?esψthen every computation of now c then A else B satis?es eitherφorψ,depending on the fact that c is an input or not.

Hiding of a local variable x is axiomatized in rule T4by?rst existentially quantifying x inφ∧loc(x),where loc(x)denotes the following formula which expresses that x is local,i.e.,the inputs of the environment do not contain new information on x:

?p(?x p=p→(?I(p)∧2( I(p)→?r(O(r)∧?x p?r=p)))).

This formula literally states that the initial input does not contain information on x and that everywhere in the computation if in the next state an input contains information on x then this information is already contained by the previous output.Finally,the following formula inv(x)

?p2(?x p=p→(O(p)→?r(I(r)∧?x p?r=p)))

states that the process does not provide new information on the global variable x.

Rule T5gives a compositional axiomatization of parallel composition.The‘fresh’constraint predicates X and Y are used to represent the outputs of A and B,respectively(φ[X/O]andψ[Y/O]denote the result of replacing O by X and Y).Additionally,the formula

?p2(O(p)?(?q1,q2(X(q1)∧Y(q2)∧q1?q2=p))),

denoted by par(X,Y),expresses that every output of A B can be decomposed into outputs of A and B.

Rule T6,where?p denotes derivability within the proof system,describes recursion in the usual manner by using a meta-rule(Scott-induction,see also[4]):we can conclude that the agent p(x)satis?es a propertyφwhenever the body of p(x)satis?es the same property assuming the conclusion of the rule. In this rule x is assumed to be both the formal and the actual parameter.We do not need more rules since,as previously mentioned,we can assumed that the set D of procedure declarations is closed wrt parameter names.

Note also that,for the sake of simplicity,we do not mention explicitly the declarations in the proof system.In fact,the more precise formulation of this rule,that will be needed in the proofs,would be the following:

D\{p}.p(x)satφ?p D\{p}.A satφ

4Soundness and completeness

We investigate now soundness and completeness of the above calculus.Here and in the following,in order to clarify some technical details,we consider processes of the form D.A rather than agents of the form A with a separate set of declarations D.All the previous de?nitions can be extended to processes in the obvious way.We also denote by?p D.A satφthe derivability of the correctness assertion D.A satφin the proof system introduced in the previous section(assuming as additional axioms in rule T7all valid temporal formulas).

Soundness means that every provable correctness assertion is valid:whenever?p D.A satφ,i.e.D.A satφis derivable,then|=D.A satφ.Completeness on the other hand consists in the derivability of every valid correctness assertion:whenever|=D.A satφthen?p D.A satφ(in T).

At the heart of the soundness and completeness results that we are going to prove lies the compositionality of the semantics R′,which follows from the compositionality of the underlying semantics R.In order to prove such a compositionality,we?rst introduce a denotational semantics[[D.A]](e)where,for technical reasons,we represent explicitly the environment e which associate a denotation to each procedure iden-ti?er.More precisely,assuming that Pvar denotes the set of procedure identi?er,Env=Pvar→?(S), with typical element e,is the set of environments.

Given a process D.A,the denotational semantics[[D.A]]:Env→?(S)is de?ned by the equations in Table3,whereμdenotes the least?xpoint wrt subset inclusion of elements of?(S).The semantic operators appearing in Table3are formally de?ned as follows.Intuitively they re?ect,in terms of reactive sequences,the operational behaviour of their syntactic counterparts.

De?nition4.1[5]Let S,S i be sets of reactive sequences and c,c i be constraints.Then we de?ne the operators? ,? ,?now and??x as follows:

Guarded Choice

? n i=1c i→S i={s·s′∈S|s= d1,d1 ··· d m,d m ,d j?c i for each j∈[1,m-1],i∈[1,n],

d m?c h and s′∈S h for an h∈[1,n]}

∪

{s∈S|s= d1,d1 ··· d m,d m ,d j?c i for each j∈[1,m],i∈[1,n]},

Parallel Composition Let? ∈S×S→S be the(commutative and associative)partial operator de?ned as follows:

c1,d1 ··· c n,d n d,d ? c1,e1 ··· c n,e n d,d = c1,d1?e1 ··· c n,d n?e n d,d .

We de?ne S1? S2as the point-wise extension of the above operator to sets.

The Now-Operator

now(c,S1,S2)={s∈S|s= c′,d ·s′and either c′?c and s∈S1or c′?c and s∈S2}.

The Hiding Operator We?rst need the following notions similar to those used in[8]:

Given a sequence s= c1,d1 ··· c n,c n ,we denote by?xs the sequence ?xc1,?xd1 ··· ?xc n,?xc n .

A sequence s′= c1,d1 ··· c n,c n is x-connected if

??x c1=c1(that is,the input constraint of s′does not contain information on x)and

??x c i?d i?1=c i for each i∈[2,n](that is,each assumption c i does not contain any information on x which has not been produced previously in the sequence by some d j).

A sequence s is x-invariant if

?for all computation steps c,d of s,d=?x d?c holds.

The semantic hiding operator then can be de?ned as follows:

??xS={s∈S|there exists s′∈S such that?

s=?x s′,s′is x-connected and s is x-invariant}.

A few explanations are in order here.Concerning the semantic choice operator,a sequence in? n i=1c i→S i consists of an initial period of waiting for(a constraint stronger than)one of the constraints c i.During this waiting period only the environment is active by producing the constraints d i while the process itself generates the stuttering steps d i,d i .Here we can add several pairs since the external environment can take several time-units to produce the required constraint.When the contribution of the environment is strong enough to entail a c h the resulting sequence is obtained by adding s′∈S h to the initial waiting period.

In the semantic parallel operator de?ned on sequences we require that the two arguments of the operator agree at each point of time with respect to the contribution of the environment(the c i’s)and that they have the same length(in all other cases the parallel composition is assumed being unde?ned).

In the de?nition of??we say that a sequence is x-connected if no information on x is present in the input constraints which has not been already accumulated by the computation of the agent itself.A sequence is x-invariant if its computation steps do not provide more information on x.

If D.A is a closed process,that is if all the procedure names occurring in A are de?ned in D,then [[D.A]](e)does not depend on e and will be indicated as[[D.A]].Environments in general allows us to de?ned the semantics also of processes which are not closed,and this will be used in the soundness proof. The following result shows the correspondence between the two semantics we have introduced and there-fore the compositionality of R(A).

Theorem4.2[5]If D.A is closed then R(A)=[[D.A]]holds.

E1[[D.stop]](e)={ c1,c1 c2,c2 ··· c n,c n ∈S|n≥1}

E2[[D.tell(c)]](e)={ d,d?c ·s∈S|s∈[[D.stop]](e)}

E3[[D. n i=1ask(c i)→A i]](e)=? n i=1c i→[[D.A i]](e)

E4[[D.now c then A else B]](e)=?

now(c,[[D.A]](e),[[D.B]](e))

E5[[D.A B]](e)=[[D.A]](e)? [[D.B]](e)

E6[[D.?xA]](e)=??x[[D.A]](e)

E7[[D.p(x)]](e)=μΨ

whereΨ(f)=[[D\{p}.A]](e{f/p}),p(x)::A∈D

Table3:The semantics[[D.A]](e).

In order to prove the soundness of the calculus we have to interpret also correctness assertions about arbitrary processes(that is,including processes which do contain unde?ned procedure variables).

De?nition 4.3Given a underlying constraint system C and an environment e ,we de?ne |=e D.A sat φi?

ρ|=φ,for all ρ∈[[D.A ]]′(e ),

where

[[D.A ]]′(e )={v 1,...,v n | v 1(I ),v 1(O ) ··· v n (I ),v n (O ) ∈[[D.A ]](e )}.

Note that,for closed processes,|=e coincides with |=as previously de?ned.We ?rst need the following Lemma.

Lemma 4.4Let φbe a temporal formula,ρand ρ′be sequences of predicate assignment and let V be a variable such that either V ∈M or V is a variable x of the underlying constraint system.The following holds:

1.Assume that ρ|=φ.Then ρ′|=?V φfor each ρ′such that ?V ρ=?V ρ′.

2.Assume that ρ|=?V φand F V constr (φ)=?.Then there exists ρ′such that ρ′|=φand ?V ρ′=?V ρ.Proof

1.Assume that ρ|=φ.By De?nition 3.3,ρ|=γφfor each γand then for each ρ′such that ?V ρ=?V ρ′,we have that ρ′|=γ?V φfor each γ.Therefore,by De?nition 3.3,ρ′|=?V φ.

2.Assume that ρ|=?V φand F V constr (φ)=?.By De?nition

3.3,ρ|=γ?V φfor each γ.Then by De?nition 3.3,for each γthere exists ρ′such that ?V ρ=?V ρ′and ρ′|=γφ.Since by hypothesis F V constr (φ)=?,whenever ρ′|=γφwe also have that ρ′|=φand then the thesis holds.

The following Theorem is the core of the soundness result.

Theorem 4.5Let us denote D i .A i by P i for 1≤i ≤n and D.A by P .If

P 1sat φ1,...,P n sat φn ?p P sat φand |=e P i sat φi ,

for i =1,...,n ,then

|=e P sat φ.

Proof The proof is by induction on the length l of the derivation.

(l =1)In this case A =tell (c )and ?p D.tell (c )sat O (c )∧?p (O (p )→?q (I (q )∧q ?c =p ))∧ 2stut .By

De?nition 4.3,we have to prove that for any e ,ρ|=O (c )∧?p (O (p )→?q (I (q )∧q ?c =p ))∧ 2stut ,for all ρ∈[[D.tell (c )]]′(e ).By equation E2of Table 3and De?nition 4.3,

[[D.tell (c )]]′(e )={ρ|ρ1(O )=ρ1(I )?c and ρi (O )=ρi (I )for i ∈[2,l (ρ)]}.

The remaining of the proof for this case is straightforward.

(l >1)We distinguish various cases according to the last rule applied in the derivation.

Rule T2.In this case ?p D. n

i =1ask (c i )→A i sat χ,where χis the formula

n i =1

(

n j =1?I (c j )∧stut )U (I (c i )∧stut ∧ φi ) ∨2(n j =1?I (c j )∧stut ).Since for each i ∈[1,n ]the proof D.A i sat φi is shorter than the current one,from the inductive hypothesis follows that,for every environment e and for each i ∈[1,n ],|=e D.A i sat φi ,that is ρ|=φi ,for all ρ∈[[D.A i ]]′(e ).

Let us take a particular e.By De?nition4.3,we have to prove thatρ|=χ,for allρ∈[[D. n i=1ask(c i)→A i]]′(e).

By equation E3of Table3and De?nitions4.1and4.3,[[D. n i=1ask(c i)→A i]]′(e)=D1∪D2, where

D1={ρ·ρ′|ρj(O)=ρj(I)andρj(I)?c i for each j∈[1,l(ρ)?1],i∈[1,n]

ρl(ρ)(I)?c h,ρl(ρ)(O)=ρl(ρ)(I)andρ′∈[[D.A h]]′(e)for an h∈[1,n]}and D2={ρ|ρj(O)=ρj(I)andρj(I)?c i for each j∈[1,l(ρ)],i∈[1,n]} Now,it is straightforward to prove that ifρ∈D2thenρ|=2( n j=1?I(c j)∧stut).Moreover, since by inductive hypothesis for each i∈[1,n],|=e D.A i satφi,we have that ifρ∈D1then ρ|= n i=1 ( n j=1?I(c j)∧stut)U(I(c i)∧stut∧ φi) and then the thesis.

Rule T3In this case?p now c then A else B sat(I(c)∧φ)∨(?I(c)∧ψ).Since the proofs

A satφand

B satψare shorter than the current one,the induction hypothesis says that for

every environment e,we have that|=e D.A satφand|=e D.B satψi.e.ρ|=φandρ′|=ψfor allρ∈[[D.A]]′(e)andρ′∈[[D.B]]′(e).

Let us take a particular e.By De?nition4.3,we have to prove thatρ|=(I(c)∧φ)∨(?I(c)∧ψ) for allρ∈[[D.now c then A else B]]′(e).Now the proof is immediate,by observing that by equation E4of Table3and De?nitions4.1and4.3,[[D.now c then A else B]]′(e)=D1∪D2, where

D1={ρ|ρ1(I)?c andρ∈[[D.A]]′(e)}and

D2={ρ′|ρ′1(I)?c andρ′∈[[D.B]]′(e)}.

Rule T4In this case?p?xA sat?x(φ∧loc(x))∧inv(x).Since the proof A satφis shorter than the current one,the induction hypothesis says that for every environment e,|=e D.A satφ

i.e.ρ′|=φfor allρ′∈[[D.A]]′(e).Let us consider a particular e.By De?nition4.3,we have

to prove thatρ|=?x(φ∧loc(x))∧inv(x),for allρ∈[[D.?xA]]′(e).By equation E6of Table3 and De?nitions4.1and4.3,ρ∈[[D.?xA]]′(e)if and only if there existsρ′∈[[D.A]]′(e)such that l(ρ)=l(ρ′)and the following conditions hold

1.for each i∈[1,l(ρ)],?xρi(I)=?xρ′i(I)and?xρi(O)=?xρ′i(O),

2.?xρ′1(I)=ρ′1(I)and for each i∈[2,l(ρ)],?xρ′i(I)?ρ′i?1(O)=ρ′i(I),

3.for each i∈[1,l(ρ)],ρi(O)=?xρi(O)?ρi(I).

Since for any sequenceρof predicate assignments and for any tccp process D.A,ρ∈[[D.A]]′(e) if and only if its‘projection’onto the distinguished predicates I and O generates a reactive sequence of D.A,by1.we can assume without loss of generality that?xρ=?xρ′.From2., the de?nition of loc(x)and the inductive hypothesis follows thatρ′|=φ∧loc(x).Therefore,by the previous equality and case1of Lemma4.4imply thatρ|=?x(φ∧loc(x))holds.Moreover by3.and by de?nition of inv(x)we obtain thatρ|=inv(x)thus proving the thesis for this case.

Rule T5In this case?p A B satχ,whereχis the formula

?X,Y(φ[X/O]∧ψ[Y/O]∧par(X,Y)),

X,Y∈M,X=Y and X,Y∈F V(φ)∪F V(ψ).Since the proofs A satφand B satψare shorter than the current one,the induction hypothesis says that for every environment e,we have that|=e D.A satφand|=e D.B satψi.e.ρ′|=φandρ′′|=ψfor allρ′∈[[D.A]]′(e)and ρ′′∈[[D.B]]′(e).

Let us take a particular e.By De?nition4.3,we have to prove thatρ|=χ,for allρ∈[[D.A

B]]′(e).Assume thatρ∈[[D.A B]]′(e).By equation E5of Table3and De?nitions4.1and

4.3,there existρ′∈[[D.A]]′(e)andρ′′∈[[D.B]]′(e)such that l(ρ)=l(ρ′)=l(ρ′′)and for

each i∈[1,l(ρ)],ρi(I)=ρ′i(I)=ρ′′i(I)andρi(O)=ρ′i(O)?ρ′i(O).Since for any sequence ρof predicate assignments and for any tccp process D.A,ρ∈[[D.A]]′(e)if and only if its ‘projection’on the distinguished predicates I and O generates a reactive sequence of D.A,by previous observation we can assume without loss of generality thatρi(Z)=ρ′i(Z)=ρ′′i(Z)for

each i∈[1,n]and for each Z∈M such that Z=O.Now we can construct a new sequence

ˉρof predicate assignments,of the same length ofρ,such thatˉρi(X)=ρ′i(O)ˉρi(Y)=ρ′′i(O)

ˉρi(Z)=ρi(Z)for each i∈[1,l(ρ)]and for each Z∈M such that Z=X,Y.Since X and Y

are not free inφandψand by inductive hypothesisρ′|=φandρ′′|=ψholds,by construction

we obtain thatˉρ|=φ[X/O]andˉρ|=ψ[Y/O].Moreover,by constructionˉρ|=par(X,Y)holds.

Thereforeˉρ|=φ[X/O]∧ψ[Y/O]∧par(X,Y)and the thesis follows from case1of Lemma4.4

by observing that?X,Yρ=?X,Yˉρ.

Rule T6In this case?p D.p(x)satφ.Since the proof D\{p}.p(x)satφ?p D\{p}.A satφis shorter than the current one,the induction hypothesis says that for every environment e such

that|=e D\{p}.p(x)satφwe also have that|=e D\{p}.A satφ.Let us take a particular e.

We have to show that|=e D.p(x)satφholds or,in other words,that ifρ∈[[D.p(x)]](e)then

we have thatρ|=φ.

Now[[D.p(x)]](e)=μΨ,whereμΨ= i f i,with f0=?and f i+1=[[D\{p}.A]](e{f i/p}).Thus

it su?ces to prove by induction that for all n,ifρ∈f n then,ρ|=φ.The base case is obvious.

Suppose that the thesis holds for f n,so for e′=e{f n/p}we have that|=e′D\{p}.p(x)satφ,

holds.Thus we infer that|=e′D\{p}.A satφ.Since by de?nition f n+1=[[D\{p}.A]](e{f n/p}),

we have that ifρ∈f n+1thenρ|=φwhich completes the proof.

Rule T7The proof is immediate.

Since R(A)=[[D.A]](e)holds for any closed process D.A with e arbitrary,whenever|=e D.A satφwe also have|=D.A satφ.Hence from the above result,with n=0,we can derive immediately the soundness of the system.

Corollary4.6(Soundness)The proof system consisting of the rules C0-C7is sound,that is,given a closed process D.A,if?p A satφthen|=D.A satφholds,for every correctness assertion D.A satφ.

Following the standard notion of completeness for Hoare-style proof systems as introduced by[13]we consider here a notion of relative completeness.We assume the existence of a property which describes exactly the denotation of a process,that is,we assume that for any process D.A there exists a formula, that for the sake of simplicity we denote byψ(A),such thatρ∈R′(A)i?ρ|=ψ(A)holds3.This is analogous to assume the expressibility of the strongest postcondition of a process P,as with standard Hoare-like proof systems.Furthermore,we assume as additional axioms all the valid temporal formulas, (for use in the consequence rule).Also this assumption,in general,is needed to obtain completeness of Hoare logics.

Analogously to the previous case,the completeness of the system is a corollary of the following Theorem.

Theorem4.7Let D={p1(x1)::A1,...,p n(x n)::A n}be a set of declarations and A an agent which involves only calls to procedures declared in D.Then we have

Φ1,...,Φn?p A satψ(A).

where,for i=1,...,n,Φi=p i(x i)satψ(p i(x i));.

Proof First observe that,for i=1,...,n,we can assume F V constr(ψ(p i(x i)))=?.In fact,from the de?nition of|=it follows thatρ∈R′(p i(x i))if and only ifρ|=γψ(p i(x i)),for each constraint assignment γ,and this holds if and only ifρ|=?constrψ(p i(x i)),where?constrψ(p i(x i))is the universal closure over

constraint variables of the formulaψ(p i(x i)).Therefore we can assume that all the constraint variables inψ(p i(x i))are universally quanti?ed,thus there are no free constraint variables.

We prove now,by induction on the complexity of A,thatΦ1,...,Φn?p A satψ(A)and F V constr(ψ(A))=?.

(tell(c))In this case,since F V constr(O(c)∧?p(O(p)→?q(I(q)∧q?c=p))∧ 2stut)=?,we have only to prove that

ψ(tell(c))=O(c)∧?p(O(p)→?q(I(q)∧q?c=p))∧ 2stut.

The proof is straightforward,since De?nition3.5,Theorem4.2and equation E2of Table3imply that the following equalities hold

R′(tell(c))={ρ|ρ1(O)=ρ1(I)?c andρi(O)=ρi(I)for i∈[2,l(ρ)]}.

(Σn i=1ask(c i)→A i)By inductive hypothesis we obtain that

Φ1,...,Φn?p A i satψ(A i)and F V constr(ψ(A i))=?,

for i=1,2,...,n.Then by rule T2we obtain also that

Φ1,...,Φn?p A satβ

where

β=

i=1

j=1

?I j∧stut)U(I i∧stut∧ ψ(A i)) ∨2(n j=1?I j∧stut),

The inductive hypothesis implies that that

F V constr(β)=?.

Then,in order to prove the thesis we have to show that

β=ψ(Σn i=1ask(c i)→A i)

holds,that is,we have to prove thatρ∈R′(Σn i=1ask(c i)→A i)if and only ifρ|=β.

(Only if).Assume thatρ∈R′(Σn i=1ask(c i)→A i).By Theorem4.2,equation E4in Table3and De?nition4.1it follows thatρ∈D1∪D2where

D1={ρ·ρ′|ρj(O)=ρj(I)andρj(I)?c i for each j∈[1,l(ρ)?1],i∈[1,n]

ρl(ρ)(I)?c h,ρl(ρ)(O)=ρl(ρ)(I)andρ′∈[[D.A h]]′for an h∈[1,n]}and D2={ρ|ρj(O)=ρj(I)andρj(I)?c i for each j∈[1,l(ρ)],i∈[1,n]} By de?nition ofψ(A)and De?nition3.5,ifρ′∈[[D.A h]]′thenρ′|=ψ(A h).Therefore,ifρ∈D1then ρ|=( n j=1?I j∧stut)U(I i∧stut∧ ψ(A h))for an h∈[1,n]which impliesρ|=βby de?nition of disjunction and ofβ.

Ifρ∈D2then clearlyρ|=2( n j=1?I(c j)∧stut)and thereforeρ|=β.This complete the proof of the“Only if”part.The proof of the other implication is analogous(by using D1and D2above) and hence omitted.

(now c then A else B)By inductive hypothesis we obtain

Φ1,...,Φn?p A satψ(A),Φ1,...,Φn?p B satψ(B)and F V constr(ψ(A))=F V constr(ψ(B))=?.

Therefore rule T3implies that

Φ1,...,Φn?p now c then A else B sat(I(c)∧ψ(A))∨(?I(c)∧ψ(B)).

Since the inductive hypothesis implies also that F V constr((I(c)∧ψ(A))∨(?I(c)∧ψ(B)))=?,to prove the thesis we have only to show that

(I(c)∧ψ(A))∨(?I(c)∧ψ(B))=ψ(now c then A else B)

hold,that is,we have to show thatρ∈R′(now c then A else B)if and only ifρ|=(I(c)∧ψ(A))∨(?I(c)∧ψ(B)).The proof is straightforward,by observing that from the de?nition ofψ(A)and ψ(B),from De?nition3.5,Theorem4.2,equation E4of Table3and De?nition4.1it follows the following equality

R′(now c then A else B)={ρ|ρ1(I)?c andρ|=ψ(A)}∪

{ρ′|ρ′1(I)?c andρ′|=ψ(B)}.

(?x A)The inductive hypothesis implies that

Φ1,...,Φn?p A satψ(A)and F V constr(ψ(A))=?

and therefore,by rule T4,we obtain that

Φ1,...,Φn?p A sat?x(ψ(A)∧loc(x))∧inv(x).

From the inductive hypothesis and the de?nitions of loc(x)and of inv(x),we obtain that

F V constr(?x(ψ(A)∧loc(x))∧inv(x))=?.(1)

In order to prove the thesis,we have then to show that

?x(ψ(A)∧loc(x))∧inv(x)=ψ(?xA),

holds,that is,we have to prove thatρ∈R′(?xA)if and only ifρ|=?x(ψ(A)∧loc(x))∧inv(x).

Assume now thatρ∈R′(?xA).De?nition3.5,Theorem4.2,equation E6of Table3,De?nition4.1 and the de?nition ofψ(A)imply that there existsρ′such thatρ′|=ψ(A),l(ρ)=l(ρ′)and the following conditions hold:

1.for each i∈[1,l(ρ)],?xρi(I)=?xρ′i(I)and?xρi(O)=?xρ′i(O);

2.?xρ′1(I)=ρ′1(I)and for each i∈[2,l(ρ)],?xρ′i(I)?ρ′i?1(O)=ρ′i(I);

3.for each i∈[1,l(ρ)],ρi(O)=?xρi(O)?ρi(I).

Now the proof is analogous to that one already given for the case of Rule T4of Theorem4.5.

Conversely,assume thatρ|=?x(ψ(A)∧loc(x))∧inv(x).Then the following facts hold:

1.ρ|=inv(x).Therefore,by de?nition of inv(x),for each i∈[1,l(ρ)]the following holds

ρi(O)=?xρi(O)?ρi(I);(2)

2.ρ|=?x(ψ(A)∧loc(x)).Then,from case2of Lemma4.4and(1)we obtain thatρ′|=

ψ(A)∧loc(x)for someρ′such that

?xρ′=?xρ.(3) Sinceρ′|=ψ(A)∧loc(x),from the de?nition ofψ(A)and of loc(x)it follows that

ρ′∈R′(A)and(4)

?xρ′1(I)=ρ′1(I)and for each i∈[2,l(ρ)],?xρ′i(I)?ρ′i?1(O)=ρ′i(I).(5) From De?nition3.5,Theorem4.2,equation E6of Table3,De?nition4.1,(2),(3),4)and(5),it follows thatρ∈R′(?xA)and therefore the thesis holds.

(A1 A2)By inductive hypothesis we obtain that

Φ1,...,Φn?p A i satψ(A i)and F V constr(ψ(A i))=?,

for i=1,2.Then by rule T5we obtain also that

Φ1,...,Φn?p A sat?X,Y(ψ(A1)[X/O]∧ψ(A2)[Y/O]∧par(X,Y)),

where X,Y∈F V(ψ(A1))∪F V(ψ(A2))and X=Y.

The inductive hypothesis and the de?nition of par(X,Y)imply that

F V constr(?X,Y(ψ(A1)[X/O]∧ψ(A2)[Y/O]∧par(X,Y))=?.(6)

Then,in order to prove the thesis we have to show that

?X,Y(ψ(A1)[X/O]∧ψ(A2)[Y/O]∧par(X,Y))=ψ(A1 A2), holds,that is,we have to prove thatρ∈R′(A1 A2)if and only ifρ|=?X,Y(ψ(A1)[X/O]∧ψ(A2)[Y/O]∧par(X,Y)).

Assume thatρ∈R′(A1 A2).By De?nition3.5,Theorem4.2,equation E4in Table3and De?nition4.1it follows that there existρ′∈R′(A1)andρ′′∈R′(A2)such that l(ρ)=l(ρ′)=l(ρ′′) and,for each i∈[1,l(ρ)],ρi(I)=ρ′i(I)=ρ′′i(I)andρi(O)=ρ′i(O)?ρ′i(O)hold.Sinceρ′∈R′(A1), the de?nition ofψ(A1)implies thatρ′|=ψ(A1).Analogously we have thatρ′′|=ψ(A2).Now the proof is analogous to that one already shown for the case of Rule T5in the proof of Lemma4.5.

Conversely,assume thatρ|=?X,Y(ψ(A1)[X/O]∧ψ(A2)[Y/O]∧par(X,Y)).We have to prove that ρ∈R′(A1 A2).By case2of Lemma4.4and(6)there exists a sequence of predicate assignments ˉρsuch that?X,Yˉρ=?X,Yρandˉρ|=ψ(A1)[X/O]∧ψ(A2)[Y/O]∧par(X,Y).

We can now construct two new sequencesρ′andρ′′of predicate assignments having the same length asˉρ,such that,for each i∈[1,l(ˉρ)],

ρ′i(O)=ˉρi(X),ρ′′i(O)=ˉρi(Y)andρ′i(Z)=ρ′′i(Z)=ˉρi(Z),for each Z∈M,Z=O.(7) Since X,Y∈F V(ψ(A1))∪F V(ψ(A2))and X=Y,by construction it follows thatρ′|=ψ(A1)and ρ′′|=ψ(A2).Therefore,by de?nition ofψ(A),

ρ′∈R′(A1)andρ′′∈R′(A2).(8) Moreover,sinceˉρ|=par(X,Y),again by construction we obtain that,for i∈[1,l(ˉρ)],

ˉρi(O)=ρ′i(O)?ρ′′i(O)(9) holds.From De?nition3.5,Theorem4.2,equation E4in Table3,De?nition4.1,(7),(8)and(9) it follows thatˉρ∈R′(A1 A2).Observe now that,by de?nition,for any sequenceρof predicate assignments and for any tccp process A,ρ∈R′(A)if and only if its‘projection’on the distinguished predicates I and O generates a reactive sequence of R(A).Hence,since?X,Yˉρ=?X,Yρand ˉρ∈R′(A1 A2),we have thatρ∈R′(A1 A2)and therefore the thesis holds.

(A=p(y))Immediate.

From the above Theorem we derive the following corollary:

Corollary4.8(Completeness)Let D={p1(x1)::A1,...,p n(x n)::A n}and A n+1be an agent such that A i,for1≤i≤n+1,only involves calls to procedures declared in D.It follows that|=D.A n+1satφimplies?p D.A n+1satφ.

Proof By the above lemma we have for i=1,...,n that

Φ1,...,Φn?p A i satψ(D.p i(x i))

whereΦi=p i(x i)satψ(D.p i(x i))(note thatψ(D.A i)=ψ(D.p i(x i))).Now a repeated application of the recursion rule gives us?p D.p i(x i)satψ(D.p i(x i)).Again by the above lemma we have that

Φ1,...,Φn?p A n+1satψ(D.A n+1)

It follows by a straightforward induction on the length of the derivation(which does not involve applica-tions of the recursion rule)that

Φ′1,...,Φ′n?p D.A n+1satψ(D.A n+1)

whereΦ′i=D.p i(x i)satψ(D.p i(x i)),i=1,...,n.So,since?pΦ′i,i=1,...,n,we thus derive that ?p D.A n+1satψ(D.A n+1).Assume now that|=D.A n+1satφ.Then|=ψ(D.A n+1)→φholds and an application of C7gives us?p D.A n+1satφ.

The formulaψ(A)(analogous to the strongest postcondition)has been used to prove completeness. However,often to prove a property of a program it is su?cient to deal with some simpler property.The situation can be compared to the problem of?nding the suitable invariant when using the standard Hoare systems for imperative programming.

5Related and future work

We introduced a temporal logic for reasoning about the correctness of a timed extension of ccp and we proved the soundness and completeness of a related proof system.

A simpler temporal logic for tccp has been de?ned in[6]by considering epistemic operators of“belief”and“knowledge”which corresponds to the operators I and O considered in the present paper.Even though the intuitive ideas of the two papers are similar,the technical treatment is di?erent.In fact,the logic in[6]is less expressive than the present one,since it does not allow constraint(predicate)variables. As a consequence,the proof system de?ned in[6]was not complete.

Recently,a logic for a di?erent timed extension of ccp,called ntcc,has been presented in[24].The language ntcc[30,23]is a non deterministic extension of the timed ccp language de?ned in[27].Its com-putational model,and therefore the underlying logic,are rather di?erent from those that we considered. Analogously to the case of the ESTEREL language,computation in ntcc(and in the language de?ned in [27])proceeds in“bursts of activity”:in each phase a ccp process is executed to produce a response to an input provided by the environment.The process accumulates monotonically information in the store, according to the standard ccp computational model,until it reaches a“resting point”,i.e.a terminal state in which no more information can be generated.When the resting point is reached,the absence of events can be checked and it can trigger actions in the next time interval.Thus,each time interval is identi?ed with the time needed for a ccp process to terminate a computation.Clearly,in order to ensure that the next time instant is reached,the ccp process has to be always terminating,thus it is assumed that it does not contain recursion(a restricted form of recursion is allowed only across time boundaries). Furthermore,the programmer has to transfer explicitly the all information from a time instant to the next one by using special primitives,since at the end of a time interval all the constraints accumulated and all the processes suspended are discarded,unless they are argument to a speci?c primitive.These assumptions allow to obtain an elegant semantic model consisting of sequences of sets of resting points (each set describing the behavior at a time instant).

On the other hand,the tccp language that we consider has a di?erent notion of time,since each time-unit is identi?ed with the time needed for the underlying constraint system to accumulate the tell’s and to

answer the ask’s issued at each computation step by the processes of the system.This assumption allows us to obtain a direct timed extension of ccp which maintain the essential features of ccp computations. No restriction on recursion is needed to ensure that the next time instant is reached,since at each time instant there are only a?nite number of parallel agents which can perform a?nite number of(ask and tell)actions.Also,no explicit transfer of information across time boundaries is needed in tccp,since the (monotonic)evolution of the store is the same as in ccp(these di?erences a?ects the expressive power of the language,see[5]for a detailed discussion).Since the store grows monotonically,some syntactic restrictions are needed also in tccp in order to obtain bounded response time,that is,to be able to statically determine the maximal length of each time-unit(see[5]).

?From a logical point of view,as shown in[4]the set of resting points of a ccp process characterizes essen-tially the strongest post condition of the program(the characterization however is exact only for a certain class of programs).In[24]this logical view is integrated with(linear)temporal logic constructs which are interpreted in terms of sequences of sets of resting points,thus taking into account the temporal evolution of the system.A proof system for proving the resulting linear temporal properties is also de?ned in[24]. Since the resting points provide a compositional model(describing the?nal results of computations),in this approach there is no need for a semantic and logical representation of“assumptions”.On the other hand such a need arises when one wants to describe the input/output behavior of a process,which for generic(non deterministic)processes cannot be obtained from the resting points.Since tccp maintains essentially the ccp computational model,at each time instant rather than a set of?nal results(i.e.a set of resting points)we have an input/ouput behavior corresponding to the interaction of the environment, which provides the input,with the process,which produces the output.This is re?ected in the the logic we have de?ned.

Related to the present paper is also[14],where tcc speci?cations are represented in terms of graph structures in order to apply model checking techniques.A?nite interval of time(introduced by the user) is considered in order to obtain a?nite behavior of the tcc program,thus allowing the application of existing model checking algorithms.

Future work concerns the investigation of an axiomatization for the temporal logic introduced in this paper and the possibility of obtaining decision procedures,for example considering a semantic tableaux method.Since reactive sequences have been used also in the semantics of several other languages,including data?ow and imperative ones[21,10,9,12],we plan also to consider extensions of our logic to deal with these di?erent languages.

References

[1]L.Aceto and D.Murphy.Timing and causality in process algebra.Acta Informatica,33(4):317-350,

1996.

[2]J.Baeten and J.Bergstra.Real time process algebra.Formal Aspects of Computing,3(2):142-188,

1991.

[3]G.Berry and G.Gonthier.The ESTEREL programming language:Design,semantics and imple-

mentation.Science of Computer Programming,19(2):87-152,1992.

[4]F.S.de Boer,M.Gabbrielli,E.Marchiori and C.Palamidessi.Proving Concurrent Constraint

Programs Correct.Transactions on Programming Languages and Systems(TOPLAS),19(5):685-725.ACM Press,1997.

[5]F.S.de Boer,M.Gabbrielli and M.C.Meo.A Timed CCP https://www.doczj.com/doc/5815017866.html,rmation and Computation,

161,2000.

[6]F.S.de Boer,M.Gabbrielli and M.C.Meo.A Temporal Logic for reasoning about Timed Concurrent

Constraint Programs.In Proc.TIME01.IEEE Press,2001.

[7]F.S.de Boer,M.Gabbrielli,and M.C.Meo.Proving correctness of Timed Concurrent Constraint

Programs.In Proc FOSSACS02.LNCS2303,Springer-Verlag,2002.

[8]F.S.de Boer,J.N.Kok,C.Palamidessi,and J.J.M.M.Rutten.On Blocks:locality and asynchronous

communication.in Proc.of REX workshop on Semantics-Foundations and Applications,vol.666 of LNCS,pages73–90.Springer-Verlag,1992.

[9]F.S.de Boer,J.N.Kok,C.Palamidessi,and J.J.M.M.Rutten.The failure of failures in a paradigm

for asynchronous communication.In J.C.M.Baeten and J.F.Groote,editors,Proceedings of CON-CUR’91,vol.527of LNCS,pages111–126.Springer-Verlag,1991.

[10]F.S.de Boer and C.Palamidessi.A Fully Abstract Model for Concurrent Constraint Programming.

In S.Abramsky and T.S.E.Maibaum,editors,Proc.of TAPSOFT/CAAP,vol.493of LNCS,pages 296–319.Springer-Verlag,1991.

[11]P.Bremond-Gregoire and I.Lee.A Process Algebra of Communicating Shared Resources with Dense

Time and Priorities.Theoretical Computer Science189,1997.

Springer-Verlag,1997.

[12]S.Brookes.A fully abstract semantics of a shared variable parallel language.In Proc.Eighth IEEE

Symposium on Logic In Computer Science.IEEE Computer Society Press,1993.

[13]S.Cook,S.Soundness and completeness of an axiom system for program veri?cation.SIAM Journal

of Computation7,1,70–90.

[14]M.Falaschi,A.Policriti,A.Villanueva.Modeling Concurrent systems speci?ed in a Temporal Con-

current Constraint language.in Proc.AGP’2000.2000.

[15]M.Fisher.An introduction to Executable Temporal Logics.Knowledge Engineering Review,6(1):

43-56,1996.

[16]N.Halbwachs,P.Caspi,and D.Pilaud.The synchronous programming language LUSTRE.In Special

issue on Another Look at Real-time Systems,Proceedings of the IEEE,1991.

[17]D.Harel.Statecharts:A Visual Formalism for Complex Systems.Science of Computer Programming

8,pages231-274,1987.

[18]L.Henkin,J.D.Monk,and A.Tarski.Cylindric Algebras(Part I).North-Holland,1971.

[19]M.Hennessy and T.Regan.A temporal process https://www.doczj.com/doc/5815017866.html,rmation and Computation,117:221-

239,1995.

[20]P.Le Guernic,M.Le Borgue,T.Gauthier,and C.Le Marie.Programming real time applications

with SIGNAL.In Special issue on Another Look at Real-time Systems,Proceedings of the IEEE, 1991.

[21]B.Jonsson.A model and a proof system for asynchronous processes.In Proc.of the4th ACM Symp.

on Principles of Distributed Computing,pages49–58.ACM Press,1985.

[22]Z.Manna and A.Pnueli.The temporal logic of reactive systems.Springer-Verlag,1991.

[23]M.Nielsen and F.D.Valencia.The ntcc Calculus and its applications.Draft,2001.

[24]C.Palamidessi and F.D.Valencia.A Temporal Concurrent Constraint Programming Calculus.In

Proc.CP01,LNCS2239,pag.302-316.Springer-Verlag,2001.

[25]V.A.Saraswat.Concurrent Constraint Programming Languages.PhD thesis,Carnegie-Mellon Uni-

versity,January1989.Published by The MIT Press,1991.

[26]V.A.Saraswat and M.Rinard.Concurrent constraint programming.In Proc.of POPL,pages

232–245.ACM Press,1990.

如何写先进个人事迹

如何写先进个人事迹篇一：如何写先进事迹材料如何写先进事迹材料一般有两种情况：一是先进个人，如先进工作者、优秀党员、劳动模范等；一是先进集体或先进单位，如先进党支部、先进车间或科室，抗洪抢险先进集体等。无论是先进个人还是先进集体，他们的先进事迹，内容各不相同，因此要整理材料，不可能固定一个模式。一般来说，可大体从以下方面进行整理。 (1)要拟定恰当的标题。先进事迹材料的标题，有两部分内容必不可少，一是要写明先进个人姓名和先进集体的名称，使人一眼便看出是哪个人或哪个集体、哪个单位的先进事迹。二是要概括标明先进事迹的主要内容或材料的用途。例如《王鬃同志端正党风的先进事迹》、《关于评选张鬃同志为全国新长征突击手的材料》、《关于评选鬃处党支部为省直机关先进党支部的材料》等。 (2)正文。正文的开头，要写明先进个人的简要情况，包括：姓名、性别、年龄、工作单位、职务、是否党团员等。此外，还要写明有关单位准备授予他(她)什么荣誉称号，或给予哪种形式的奖励。对先进集体、先进单位，要根据其先进事迹的主要内容，寥寥数语即应写明，不须用更多的文字。然后，要写先进人物或先进集体的主要事迹。这部分内容是全篇材料

的主体，要下功夫写好，关键是要写得既具体，又不繁琐；既概括，又不抽象；既生动形象，又很实在。总之，就是要写得很有说服力，让人一看便可得出够得上先进的结论。比如，写一位端正党风先进人物的事迹材料，就应当着重写这位同志在发扬党的优良传统和作风方面都有哪些突出的先进事迹，在同不正之风作斗争中有哪些突出的表现。又如，写一位搞改革的先进人物的事迹材料，就应当着力写这位同志是从哪些方面进行改革的，已经取得了哪些突出的成果，特别是改革前后的．经济效益或社会效益都有了哪些明显的变化。在写这些先进事迹时，无论是先进个人还是先进集体的，都应选取那些具有代表性的具体事实来说明。必要时还可运用一些数字，以增强先进事迹材料的说服力。为了使先进事迹的内容眉目清晰、更加条理化，在文字表述上还可分成若干自然段来写，特别是对那些涉及较多方面的先进事迹材料，采取这种写法尤为必要。如果将各方面内容材料都混在一起，是不易写明的。在分段写时，最好在每段之前根据内容标出小标题，或以明确的观点加以概括，使标题或观点与内容浑然一体。最后，是先进事迹材料的署名。一般说，整理先进个人和先进集体的材料，都是以本级组织或上级组织的名义；是代表组织意见的。因此，材料整理完后，应经有关领导同志审定，以相应一级组织正式署名上报。这类材料不宜以个人名义署名。写作典型经验材料-般包括以下几部分： (1)标题。有多种写法，通常是把典型经验高度集中地概括出来，一

机票预订管理规定

机票预订管理制度第一条总则（一）目的为进一步规范公司机票预订工作，加强飞机票预订管理，以合理控制公司费用支出，特制订本制度。（二）适用范围本制度适用于公司各部门、各区域公司和专业公司。（三）机票预订审批人申请人所属部门负责人，分管领导，常务副总经理。第二条机票预订规定（一）机票预定审批 1.有以下情形的由部门经理负责审批: 1.1机票价格不高于高铁二等票价格的； 1.2公司统一安排出行的； 1.3乘坐高铁、动车等其他交通工具时间超过12个小时的。 2.有以下情形的由分管领导审批: 2.1 公司中层管理人员需乘坐飞机的； 2.2行程紧急，高铁动车等交通工具均无法满足要求； 2.3陪同重要客户出行； 3.其他特殊情形需常务副总经理审批。（二）机票预订职责 1.公司员工公务出行的机票统一由综合管理部负责预定。 2.综合管理部负责机票信息的查询，票务公司的选择及机票预订手续的办理。原则上流程审批到前台文员处，0.5个工作日内需将最佳航班信息反馈给申请人。

3.机票出票后，前台文员负责邮件发送行程确认单和电子机票给乘机人。 4.综合管理部负责制订机票预订的流程和规定。（三）机票预订流程 1.飞机票预订必须遵守“先申请后发生”的原则，同时由于机票的价格越早预订价格越优惠的特性，故需求人应提早做好出行计划安排，同时在保证工作、出行不受影响的情况下，出行时间应遵循“早”出晚“归”，价格遵循最低航班原则，以此合理控制费用成本。除特殊情形外，需求人原则上应至少提前2天填写OA《票务预订流程》，根据具体情形选择适当的审批人，并主动跟踪审批流程至审批通过。流程图： 2.审批通过后由前台文员负责购买，前台文员收到经审批的《票务预订流程》后，及时根据预订者的要求进行机票查询及预订工作，同时做好登记，以备后续票务查询及对账工作，出票后需将机票行程确认单和电子机票提供给申请预订者。（四）机票预订要求 1.前台文员与公司签订机票预订协议的票务公司预订机票。订票时，在满足预订者出行要求的前提下，要本着安全和节约的原则进行预订。 2.前台文员在预订机票时需与票务公司核对清楚预订者提供的个人信息，并以书面传真的方式与票务公司确认。在特殊情况下（如夜间或节假日期间）前台文员可以以口头形式通知票务公司办理相关机票手续（包括

报销系统使用说明

使用说明目录使用说明 (1) 1.1. 访问系统 (2) 1.2. 系统登录与退出 (2) 1.2.1. 登录系统 (2) 1.2.2. 退出系统 (3) 1.2.3. 个人信息 (3) 1.2.4. 信息动态 (5) 1.2.5. 全局搜索 (6) 1.3. 单据的填写 (7) 1.3.1. 借款单 (7) 1.3.2. 还款单 (9) 1.3.3. 差旅费用报销 (10) 1.4. 借款单状态 (12) 1.5. 业务办理 (14) 1.6. 我的申请单 (15) 1.7. 草稿箱 (16) 1.8. 单据查询 (18) 1.9. 审批委托 (19)

1.1.访问系统在浏览器输入系统访问地址,进入登录页面，如下图所示: 图1系统登录页面 1.2.系统登录与退出 1.2.1.登录系统使用普通员工帐号登录。如用户名MZHU04，密码joinfun，登陆成功进入普通员工界面，菜单如下：图2普通员工页面

图3退出系统 1.2.3.个人信息进入主页面，移动鼠标至左上方的名字上，可以查看到个人信息数据。如下图：图4个人信息（1） 1.个人信息：点击【个人信息】，进入个人信息页面：查看当前登录人的相关信息，如需切换显示语言，在语言处选择需要显示的语言并点击“更新”。如下图：

图5个人信息（2） 2.邮件通知设置：系统审批单据时，单据签收、申请、完成、退回，拒绝等系统都会发送邮件通知，可以点击【邮件设置】选择需要发送的邮件通知。如下图：图6邮件设置（1）系统默认是7种通知类型并默认全部接收。如果您不需要接收哪种类型的邮件，点击取消选中。如下图：

费用报销系统操作手册-流程新建

三全食品费用报销系统用户操作手册日期:2019-5-17 版本: 1.0

第一章：概述第二章：系统操作 1、差旅费申请 2、会务费申请 3、日常费用报销 4、对公付款 5、费用事前申请第三章：注意事项

第一章：费用报销系统概述费用报销系统用于日常费用报销相关流程的提交。业务范围：交通邮电、行政办公、物流仓储、福利、招待等日常费用及客诉费；流程范围：事前申请、费用报销、对公付款。销售区域，此范围内流程通过ＥＫＰ费用报销模块提交流程。第二章：系统操作 1、差旅费申请 1.1路径：登录EKP——工作台——常用流程——费用报销（销售区域）——出差申请 1.2步骤：在出差申请表单填写申请文档，经领导审批后续报销时，在我的待办事项中点击此条差旅申请的报销流程，点击“编辑”，填

写出差事由、费用明细、出差报告等内容，检查收款账户信息，提交流程。 1.3差旅费明细填写小贴士： 1.3.1出差地填写时，在选择框输入出差城市关键字，可快速搜索城市，选中，确定；可选地域为市、县。 1.3.2住宿费填写天数；金额栏填写含税金额；若为专票，税额栏填写进项税额；市内交通、伙食费填写天数，实际报销金额；根据出差乘坐交通工具，将金额填在对应交通工具栏下（鼠标放在交通工具栏上可以看到详细交通工具说明）；差旅自驾产生费用填在自驾栏里；差旅过程产生其他费用在杂费栏填列。 2、会务费申请 2.1路径：登录EKP——工作台——常用流程——费用报销（销售区域）——会务费申请 2.2步骤：在会务费申请表单填写申请文档，经领导审批后续报销时，在我的待办事项中点击此条会务申请的报销流程，点击“编辑”，填写费用明细等内容，上传必要附件，检查收款账户信息，提交流程。 3、日常费用报销 3.1路径：登录EKP——工作台——常用流程——费用报销（销售区域）——通用费用报销 3.2步骤： 3.2.1选择对应报销类别

机票分哪几种

一、机票分哪几种？有什么区别？机票分为航空公司的本票和BSP中性客票。航空公司的本票用于出具本航或指定航空公司的机票，形式为纸质、硬卡、电子等；BSP中性客票通常由代理人销售，可以开具各航空公司机票，由于国际航协已经停发了BSP中性客票的纸票，目前我们所买到的BSP中性客票都是电子客票。二、经济舱、公务舱和头等舱具体有什么区别？经济舱、公务舱和头等舱在机票价格、限制条件、机舱位置、服务标准、餐食、登机顺序、行李额上都有区别。头等舱一般设在客舱的前部，座椅本身的尺寸和前后之间的间距都比较大，长航线甚至会采用平躺式座椅，相对舒适；经济舱的座位设在从机身中间到机尾的地方，占机身的四分之三空间或更多，座位尺寸相对小；公务舱介于两者之间。多数航空公司会设有头等舱和公务舱的专用休息室和特殊通道；国内航班上公务舱的客票价格是经济舱的1.3倍，头等舱客票价格是经济舱的1.5倍。头等舱和公务舱行李额相对较多，优先上机，餐食也较经济舱要丰盛。但是各家航空公司并非所有机型都设置这3种舱位。三、什么是“三不准”机票？不准签转、不准更改、不准退票。不可签转：指出票后不能更改航空公司。不可更改：指出票后不能更改日期或航班。不可退票：指出票后不能退票。四、什么叫“代码共享”？代码共享（code-sharing）是指一家航空公司的航班号（即代码）可以用在另一家航空公司的航班上。这对航空公司而言，不仅可以在不投入成本的情况下完善航线网络、扩大市场份额，而且越过了某些相对封闭的航空市场的壁垒。对于旅客而言，则可以享受到更加便捷、丰富的服务，比如众多的航班和时刻选择，一体化的转机服务、优惠的环球票价，共享的休息厅以及常旅客计划等等。五、国际票的OK票和OPEN票各是指什么？ 1、国际票按状态的不同可分为OK票和OPEN票两种，OK票（定期票）：是指返程机票航班、座位等级、乘机日期和起飞时间均订妥的机票。OPEN票（不定期票）：适用于往返程，去程订妥，回程航班、乘机日期和起飞时间都没有确定的机票。 2、常规来说机票时间来回程间隔最长是一年（OPEN票居多）； 3、机票上的回程段标有open字样，乘客确定回程日期后需尽早联系航空公司预订机位。六、国际机票有哪几种乘客类型？ 1、普通旅客 2、新移民—须提供乘客的签证以各航空公司规定为准 3、留学生—须提供乘客的入学通知书、学生签证的复印件，具以各航空公司规定为准 4、劳务人员—须提供乘客的护照以及劳务签证的复印件 5、海员—须提供海员签证复印件 6、外交官——须提供外交官护照复印件

金蝶费用预算及报销系统操作手册-财务操作手册V2.1

费用预算控制及报销系统（财务人员操作手册）越秀地产财务管控系统升级优化项目组 2014年12月

目录 1出纳操作 (3) 1.1系统客户端登录 (3) 1.2出纳业务处理 (4) 1.2.1借款单、费用报销单付款 (4) 1.2.2取消付款 (7) 1.2.3借款单还款 (8) 1.2.4取消还款 (11) 1.2.5委托其他公司代付款 (11) 1.2.6银企对私支付 (12) 1.2.7除费用报销外的付款单 (13) 1.2.8收款单 (15) 2财务会计操作 (17) 2.1系统客户端登录 (17) 2.2会计生成付款或还款 (17) 2.3会计生成冲借支凭证 (20)

1出纳操作 1.1 系统客户端登录打开金蝶EAS客户端登录界面如下：在功能菜单中点击“财务会计”→“费用管理”可以查询及处理借款单、费用报销单、出差借款单、差旅报销单；确认所在组织是否是需要进行业务处理的组织，否则需要通过EAS登陆后主界面下方点击公司名称进行切换：

1.2 出纳业务处理 1.2.1 借款单、费用报销单付款对借款单或费用报销单进行付款，确认将付款进行支付处理；出纳根据已经审批通过的借款单或费用报销单进行付款；菜单路径：方式一：“财务会计”→“出纳管理”→“付款单查询”（只能处理当前组织的付款业务）方式二：“财务共享”→“出纳共享”→“多组织付款处理”（此处可以进行多个公司付款业务，需要授权许可）

以上两种方式，单据操作相同。步骤1：在付款单的查询条件中设定查询条件，通过“分录备注”查询特定付款单。步骤2：在序时簿中，选择需要处理的付款单，点击“修改”填写付款账户、付款科目、分录预算项目，提交。注：若支付的是借款，付款单类型为个人借款；若支付的是报销款，付款单类型为费用报销。

机票预订管理规定

1.飞机票预订必须遵守“先申请后发生”的原则，同时由于机票的价格越早预订价格越优惠的特性，故需求人应提早做好出行计划安排，同时在保证工作、出行不受影响的情况下，出行时间应遵循“早”出晚“归”，价格遵循最低航班原则，以此合理控制费用成本。除特殊情形外，需求人原则上应至少提前2天填写OA《票务预订流程》，根据具体情形选择适当的审批人，并主动跟踪审批流程至审批通过。流程图： 2.审批通过后由前台文员负责购买，前台文员收到经审批的《票务预订流程》后，及时根据预订者的要求进行机票查询及预订工作，同时做好登记，以备后续票务查询及对账工作，出票后需将机票行程确认单和电子机票提供给申请预订者。（四）机票预订要求 1.前台文员与公司签订机票预订协议的票务公司预订机票。订票时，在满足预订者出行要求的前提下，要本着安全和节约的原则进行预订。 2.前台文员在预订机票时需与票务公司核对清楚预订者提供的个人信息，并以书面传真的方式与票务公司确认。在特殊情况下（如夜间或节假日期间）前台文员可以以口头形式通知票务公司办理相关机票手续（包括改期，退票，改行程等），但事后申请人返回公司当天需补发OA《机票预订流程》进行流程审批，说明原因，前台文员需与票务公司传真予以确认。若因申请机票预订者提供的个人信息错误导致出现错票或者因申请机票预订者

个人先进事迹简介

个人先进事迹简介 01 在思想政治方面,xxxx同学积极向上,热爱祖国、热爱中国共产党,拥护中国共产党的领导.利用课余时间和党课机会认真学习政治理论,积极向党组织靠拢. 在学习上,xxxx同学认为只有把学习成绩确实提高才能为将来的实践打下扎实的基础,成为社会有用人才.学习努力、成绩优良. 在生活中,善于与人沟通,乐观向上,乐于助人.有健全的人格意识和良好的心理素质和从容、坦诚、乐观、快乐的生活态度,乐于帮助身边的同学,受到师生的好评. 02 xxx同学认真学习政治理论,积极上进,在校期间获得原院级三好生,和校级三好生,优秀团员称号,并获得三等奖学金. 在学习上遇到不理解的地方也常常向老师请教,还勇于向老师提出质疑.在完成自己学业的同时,能主动帮助其他同学解决学习上的难题,和其他同学共同探讨,共同进步. 在社会实践方面,xxxx同学参与了中国儿童文学精品“悦”读书系,插画绘制工作,xxxx同学在班中担任宣传委员,工作积极主动,认真负责,有较强的组织能力.能够在老师、班主任的指导下独立完成学院、班级布置的各项工作. 03 xxx同学在政治思想方面积极进取,严格要求自己.在学习方面刻苦努力,不断钻研,学习成绩优异,连续两年荣获国家励志奖学金；作

为一名学生干部,她总是充满激情的迎接并完成各项工作,荣获优秀团干部称号.在社会实践和志愿者活动中起到模范带头作用. 04 xxxx同学在思想方面,积极要求进步,为人诚实,尊敬师长.严格要求自己.在大一期间就积极参加了党课初、高级班的学习,拥护中国共产党的领导,并积极向党组织靠拢. 在工作上,作为班中的学习委员,对待工作兢兢业业、尽职尽责的完成班集体的各项工作任务.并在班级和系里能够起骨干带头作用.热心为同学服务,工作责任心强. 在学习上,学习目的明确、态度端正、刻苦努力,连续两学年在班级的综合测评排名中获得第1.并荣获院级二等奖学金、三好生、优秀班干部、优秀团员等奖项. 在社会实践方面,积极参加学校和班级组织的各项政治活动,并在志愿者活动中起到模范带头作用.积极锻炼身体.能够处理好学习与工作的关系,乐于助人,团结班中每一位同学,谦虚好学,受到师生的好评. 05 在思想方面,xxxx同学积极向上,热爱祖国、热爱中国共产党,拥护中国共产党的领导.作为一名共产党员时刻起到积极的带头作用,利用课余时间和党课机会认真学习政治理论. 在工作上,作为班中的团支部书记,xxxx同学积极策划组织各类团活动,具有良好的组织能力. 在学习上,xxxx同学学习努力、成绩优良、并热心帮助在学习上有困难的同学,连续两年获得二等奖学金. 在生活中,善于与人沟通,乐观向上,乐于助人.有健全的人格意识和良好的心理素质.

机票管理规定(精编文档).doc

【最新整理，下载后即可编辑】机票订票管理规定第一章目的第一条为规范部门机票预订操作，合理利用订票资源，控制成本，有效实现费用节省，特制定本规定。第二章适用范围第二条本规定适用于全体人员的机票订购业务。第三章主管部门及职责第三条内务组订票人员负责机票订票业务统筹管理。第四条部门订票申请人通过出差申请单和机票申请单发起机票预订申请，部门负责人审核订票需求是否符合规定，及差旅计划是否合理。第五条订票人员依据申请单中的机票信息进行订票。第四章机票预订的相关规定第六条按照《事业单位差旅报销标准》中的相关费用标准执行。第七条无特殊情况，出差人员一律乘坐经济舱，如有特殊情况需办理升舱，需提交部门负责人和分管领导审批。第八条流程适用范围（一）出差申请单：适用于因公出差人员的往返程机票申请。（二）机票预订单：适用于订票需求，原定回程行程全部变更的机票申请、邀请的外部人员及代订的自费机票。第九条预订

（一）申请人：机票预订需提前2天以上发起流程至订票人员处进行预订，且优先选择当天折扣低的机票。（二）订票：综合如下两方因素考评后推出最终预订机票，若无更优选择，订票人员则按申请人提交申请预订机票，订票人员接到完整订票信息后立即安排订票，在2小时内必须完成订票事宜并及时以短信方式回复出差人员所定机票的具体航班信息。出差人员接到订票人发回的订票短信后，必须以短信或电话方式回复订票人。 1.根据申请人提出的班次时间在上下浮动一个小时内推出最优折扣的推荐航班班次后与申请人再次确认，若申请人支持推荐班次则订票人员按推荐班次预订。 2.订票人员推出的推荐班次通过签约机票供应商多方比价后，选择价优供应商订票。 3.如因订票人员发送的订票信息错误导致误机或改签等情况，所产生的损失一律由订票人员全额承担。（三）如预订由公司承担的外部人员机票费用，申请人需在申请单中注明费用归属科目；如为代订自费机票，则申请人需将票款交至订票人员处。（四）通过网上订票查询，若机票折扣在6折以上，需经申请由订票人员统一预订，员工不得自行预订，产生费用由订票人员统一结算。若机票折扣在6折及以下，员工可自行预订，自行预订需发起出差申请单或机票预订单，通过审批后方可执行。（五）原则上员工家属不可参与公司订票，若有特殊需求可代为预订，代订机票需发起机票预定单经过审批后由订票人员代为订票，费用由员工自行承担，申请人需按本规定中将票款交至

(财务报销管理)财务网上报销系统用户使用手册(V版)

（财务报销管理）财务网上报销系统用户使用手册(V 版)

中国石油财务网上报销系统用户使用手册

网上报销项目组 2010年5月目录目录2 1. 概述4 1.1目的及意义4 1.2适用对象及范围4 2. 系统登录4 3. 任务管理5 3.1待办单据列表5 3.2 提交单据列表7 3.3 单据审批委托7 3.4 修改本人信息8 4. 系统操作流程介绍9 5. 功能模块说明10 5.1 业务申请10 5.2 报销业务21

5.2.1 借款申请22 5.2.2 差旅费报销25 5.2.3 探亲费报销31 5.3.4 专项业务支出报销37 5.2.5 办公费报销42 5.2.6 会议费报销47 5.2.7 招待费报销52 5.2.8 运费仓储费报销57 5.2.9 医疗费报销62 5.2.10付款申请67 5.2.11还款申请70 5.2.12劳务费发放73 5.2.13通讯费报销78 5.3 查询功能83 5.3.1 个人单据查询83 5.3.2 个人借款查询84 5.3.3 个人经费查询85 5.3.4 个人机票查询86 5.3.5 个人薪资查询87 5.3.6 个人通讯费查询88 5.3.7部门单据查询88 5.3.8 部门借款查询89

5.3.9 部门经费查询90 5.3.10 部门流程查询91 5.3.11部门机票查询92 5.3.12会计机票查询92 5.3.13部门人员经费查询93 5.3.14部门单据处理查询94 5.3.15部门经费统计查询95 5.3.16部门通讯费查询96 5.3.17差旅费关联出差申请单查询96 5.3.18 薪资查询97

网上报销操作手册(3.0 版)

网上报销操作手册（3.0版） 1.登录阶段(在公司外情况下先登录VPN，在院内网环境下跳过1.1直接输入网址登录) 1.1点击桌面VPN图标，登录VPN。 1.2登录VPN后登录公司项目管理系统，网址http://10.0.6.141:7788/，输入自己的工号、密码。（推荐使用谷歌浏览器，IE或360请使用高版本，以免页面显示有误影响使用）

1.3进入网址页面后，点击右上角当前层级，选择自己相对应的项目部。 1.4在网页左侧选项中，选择资金成本—报销管理，选择相对应审批单。除差旅费报销要使用差旅费用审批单，其他报销一律使用费用报销审批单。

1.5在右上角个人姓名处点击选择个人设置，在页面选择个人信息，录入本人的手机号、工号、开户行、银行卡号等信息。保存后，今后报销中这些信息会自动生成，避免手工重复录入。 2.报销阶段 2.1点击新增增加报销事项，开始报销流程。具体流程分为四步。

2.2第一步：填写页面基本信息，灰色框格为自动生成不需要填写，其余框格需要填写。其中标题、联系电话、报销选择为必填项（不填无法保存）。报销选择为报销的，如图必须填写开户银行、银行账号及开户人，若已在个人信息处维护过相关信息，选择报销后将自动填充，若有变化，直接修改即可。 2.3报销选择必须严格按照业务类别进行选择,具体流程选择规定如下：

①采购业务：主要针对机关及项目发生的采购业务，按公司规定需要经由设备物资部审批的事项。 ②招待/车辆：主要针对业务招待费报销；公司及项目车辆发生的费用。 ③成本/税金：主要针对项目所发生的除差旅费、车辆费用、材料费、业务招待费等以外的成本开支。包括项目日常发生的快递费、打印费、水电费、伙食费等各类费用。 ④投标经营：主要针对招标、投标等业务发生的费用如：标书费、中标服务费。 ⑤安全经费：主要针对符合公司安全经费使用规定的各项费用支出。 ⑥法律/监察：主要包括：诉讼费、审计费。 ⑦技术科研：主要针对公司技术科研方面发生的费用支出。 ⑧培训：主要针对符合公司人力资源部规定的培训、学习费用报销。安全相关的培训符合规定的应当走安全经费流程报销。 ⑨其他：主要针对机关费用报销如：快递费、打印费、打车费、图书资料、电话费、水电费、物业费、团青党务费用等其他，项目部报销不使用。 2.4报销单标题应为XXX报销XXX项目XXX费用，经手人必须为票据实际经手人！录入人是根据系统当前登录用户自动提取的，无法填写

公司员工订购机票管理规定

公司员工订购机票管理规定为了加强公司内控管理，控制成本支出，提高办事效率，规范公司机票订购流程，结合公司的实际情况，特制定本规定： 1、公司高管（总经理级及以上）可直接安排行政部订购机票。 2、员工、部门经理非紧急情况出差，火车能够在15小时内到达的，原则上乘坐火车。如情况紧急，部门经理需经总经理批准后方可订购。员工出差须经本部门经理及总经理批准，方可订购机票。 3、飞机票订购说明：飞机票越早订购，折扣机票的选择机会越多，但折扣越大的机票（便宜的机票）如退改签，则退改签的费用也越高；特价机票不能退/改签，并且有出票时间限制。 4、申请人尽量把行程定下来后再通知订票，免得中途退票或改签，产生不必要的费用。 5、中途退票或改签的，需填写《退/改签申请单》说明原因，由部门领导审核签字确认。如因出差人员工作计划性不强等个人原因导致退/改签而产生额外费用的，费用由申请人承担并计入绩效考核。 6、机票申请人在确定出差时间后，原则上须提前一周填写《机票订购申请单》，经相应主管审批后，由行政部根据申请单订购机票。如因时间紧急，经主管领导批准，可先订票，但一天内需补上申请单。 7、公司与票务公司签订机票订购协议，公司员工出差机票统一由行政部负责订购机票，并对票务信息进行详细记载，以方便统计费

用并做费用分摊。 8、行政部根据当日的机票折扣，购买相近时间低折扣的机票，如乘机人指定的航班与相近时间航班的折扣相同，可购买乘机人指定的航班。 9、行政部负责每月机票费用的统计汇总，并做部门费用分摊，交财务结账。附件：《机票订购申请单》《机票退/改签申请单》编制：审核：批准：

优秀党务工作者事迹简介范文

优秀党务工作者事迹简介范文优秀党务工作者事迹简介范文 ***，男，198*年**月出生，200*年加入党组织，现为***支部书记。从事党务工作以来，兢兢业业、恪尽职守、辛勤工作，出色地完成了各项任务，在思想上、政治上同党中央保持高度一致，在业务上不断进取，团结同事，在工作岗位上取得了一定成绩。一、严于律己，勤于学习作为一名党务工作者，平时十分注重知识的更新，不断加强党的理论知识的学习，坚持把学习摆在重要位置，学习领会和及时掌握党和国家的路线、方针、政策，特别是党的十九大精神，注重政治理论水平的提高，具有坚定的理论信念;坚持党的基本路线，坚决执行党的各项方针政策，自觉履行党员义务，正确行使党员权利。平时注重加强业务和管理知识的学习，并运用到工作中去，不断提升自身工作能力，具有开拓创新精神，在思想上、政治上和行动上时刻同党中央保持高度一致。二、求真务实，开拓进取在工作中任劳任怨，踏实肯干，坚持原则，认真做好学院的党务工作，按照党章的要求，严格发展党员的每一个步骤，认真细致的对待每一份材料。配合党总支书记做好学院的党建工作，完善党总支建设方面的文件、材料和工作制度、管理制度等。

三、生活朴素，乐于助人平时重视与同事间的关系，主动与同事打成一片，善于发现他人的难处，及时妥善地给予帮助。在其它同志遇到困难时，积极主动伸出援助之手，尽自己最大努力帮助有需要的人。养成了批评与自我批评的优良作风，时常反省自己的工作，学习和生活。不但能够真诚的指出同事的缺点，也能够正确的对待他人的批评和意见。面对误解，总是一笑而过，不会因为误解和批评而耿耿于怀，而是诚恳的接受，从而不断的提高自己。在生活上勤俭节朴，不铺张浪费。身为一名老党员，我感到责任重大，应该做出表率，挤出更多的时间来投入到**党总支的工作中，不找借口，不讲条件，不畏困难，将总支建设摆在更重要的位置，解开工作中的思想疙瘩，为攻坚克难铺平道路，以支部为纽带，像战友一样团结，像家庭一样维系，像亲人一样关怀，践行入党誓言。把握机遇，迎接挑战，不负初心。

中国石油财务网上报销系统用户使用手册范本

中国石油财务网上报销系统用户使用手册网上报销项目组 2010年5月目录目录 (1) 1. 概述 (4)

1.1目的及意义 (4) 1.2适用对象及围 (4) 2. 系统登录 (4) 3. 任务管理 (5) 3.1待办单据列表 (5) 3.2 提交单据列表 (7) 3.3 单据审批委托 (7) 3.4 修改本人信息 (8) 4. 系统操作流程介绍 (9) 5. 功能模块说明 (10) 5.1 业务申请 (10) 5.2 报销业务 (21) 5.2.1 借款申请 (22) 5.2.2 差旅费报销 (25) 5.2.3 探亲费报销 (31) 5.3.4 专项业务支出报销 (37) 5.2.5 办公费报销 (42) 5.2.6 会议费报销 (47) 5.2.7 招待费报销 (52) 5.2.8 运费仓储费报销 (57) 5.2.9 医疗费报销 (62) 5.2.10付款申请 (67) 5.2.11还款申请 (70) 5.2.12劳务费发放 (73) 5.2.13通讯费报销 (78) 5.3 查询功能 (83) 5.3.1 个人单据查询 (83) 5.3.2 个人借款查询 (84) 5.3.3 个人经费查询 (85) 5.3.4 个人机票查询 (86) 5.3.5 个人薪资查询 (87) 5.3.6 个人通讯费查询 (88) 5.3.7部门单据查询 (88) 5.3.8 部门借款查询 (89) 5.3.9 部门经费查询 (90) 5.3.10 部门流程查询 (91) 5.3.11部门机票查询 (92) 5.3.12会计机票查询 (92) 5.3.13部门人员经费查询 (93) 5.3.14部门单据处理查询 (94) 5.3.15部门经费统计查询 (95) 5.3.16部门通讯费查询 (96) 5.3.17差旅费关联出差申请单查询 (96) 5.3.18 薪资查询 (97)

主要事迹简介怎么写(2020年最新)

主要事迹简介怎么写概括?简要地反映?个单位(集体)或个?事迹的材料。简要事迹不?定很短，如果情况多的话，也有?千字的。简要事迹虽然“简要”，但切忌语?空洞，写得像?学?期末鉴定。 ?应当以事实来说话。简要事迹是对某单位或个?情况概括?简要地反映情况，?如有三个??很突出，就写三个??，只是写某???时，要把主要事迹突出出来。简要事迹?般来说，?少要包括两个??的内容。?是基本情况。简要事迹开头，往往要??段?字来表述?些基本情况。如写?个单位的简要事迹，应包括这个单位的?员、承担的任务以及?段时间以来取得的主要成绩。如写个?的简要事迹，应包括该同志的性别、出?年?、参加?作时间、籍贯、民族、?化程度以及何时起任现职和主要成绩。这样上级组织在看了材料的开头，就会对这个单位或个?有?个基本印象。?是主要特点。这是简要事迹的主体部分，最突出的事例有?个??就写成?块，并按照?定的逻辑关系进 ?排列，把同类的事例排在?起，?个??通常由?个?然段或?个?然段组成。写作时，特别要注意以下四点： 1.?第三?称。就是把所要写的对象，是集体的?“他们”来表述，是个?的称之为“他(她)”。 (她)”，单位可直接写名称，个?可写其姓名。为了避免连续出现?个“他们”或“他 2.掌握好时限。?论是单位或个?的简要事迹，都有?个时间跨度，既不要扯得太远，也不要故意混淆时间概念，把过去的事当成现在的事写。这个时间跨度多长，要根据实际情况 ?定。如上级要某个同志担任乡长以来的情况就写他任乡长以来的事迹;上级要该同志两年来的情况，就写两年来的事迹。当然，有时为了需要，也可适当地写?点超过这个时间的背景情况。 3.?点他?的语?。就是在写简要事迹时，可?些群众的语?或有关?员的语?，这样会给??种?动、真切的感觉，衬托出写作对象?较?的思想境界。在?他?语?时，可适当加?，但不能造假。 4.?事实说话。简要事迹的每?个??可分为多个层次，?个层次先??句话作为观点，再???两个突出的事例来说明。?事实说话时，要尽量把?个事例说完整，以给?留下深刻印象。

机票知识(各种退改签以及营运规定)

机票知识 1、根据来源机票分哪几种？有什么区别？机票根据来源分为航空公司的本票和BSP中性客票。航空公司的本票用于出具本航或指定航空公司的机票，形式为纸质、硬卡、电子等；BSP中性客票通常由代理人销售，可以开具各航空公司机票，由于国际航协已经停发了BSP中性客票的纸票，目前我们所买到的BSP中性客票都是电子客票。 2、经济舱、公务舱和头等舱具体有什么区别？经济舱、公务舱和头等舱在机票价格、限制条件、机舱位置、服务标准、餐食、登机顺序、行李额上都有区别。头等舱一般设在客舱的前部，座椅本身的尺寸和前后之间的间距都比较大，长航线甚至会采用平躺式座椅，相对舒适；经济舱的座位设在从机身中间到机尾的地方，占机身的四分之三空间或更多，座位尺寸相对小；公务舱介于两者之间。多数航空公司会设有头等舱和公务舱的专用休息室和特殊通道；国内航班上公务舱的客票价格是经济舱的1.5倍，头等舱客票价格是经济舱的1.8倍。头等舱和公务舱行李额相对较多，优先上机，餐食也较经济舱要丰盛。但是各家航空公司并非所有机型都设置这3种舱位。 3、什么是“三不准”机票？不准签转、不准更改、不准退票。不可签转：指出票后不能更改航空公司。不可更改：指出票后不能更改日期或航班。不可退票：指出票后不能退票。 4、航空公司的票价等级是如何划分的？国内机票：票价级别是以机票价格（折扣）来划分。依次分为：头等舱，公务舱，经济舱以及经济舱以下的子舱位。 1、航空公司票价一般分为头等舱、公务舱和经济舱三种等级。每种等级依据票价的不同、旅客类型的不同及旅行的有效期长短用不同的英文字母表示。 2、头等舱代号一般为F、A、P等；公务舱代号一般为C、D、J、Z等；经济舱的代号较多，一般为：Y、M、N、L、K、V、X、T等。 3、不同的舱位代号都有对应票价和限制条件，分别拥有不同的座位数量。 4、世界上各个航空公司在舱位代号的选择上无统一的规定。旅客只要预订了规定的舱位，就可使用相应的价格。 4、经济舱不同价格的机票座位有差异吗？

武汉理工大学网上报账指南

武汉理工大学网上报账系统操作说明为进一步推进我校财务信息化工作，不断提高财务管理水平，更好地服务全校师生员工，计财处即将启用网上财务综合信息系统，该系统集合了网上报账系统、酬金发放管理系统、网上查询系统等，现就网上报账系统的使用说明如下：一、系统使用环境要求及相关准备工作请确认您使用的计算机屏幕分辨率至少为1024*768，使用WindowsXP 及以上操作系统，采用IE7.0 及以上版本浏览器（也可以使用金山浏览器、搜狗浏览器），并连接校园网络。为保证数据及时、有效性，请将浏览器“Internet 选项”->“常规”->“Internet 临时文件和历史记录设臵”中的“Internet 临时文件”，修改为“每次访问网页时”。注：财务数据多行、多列表格显示的情况较多，在浏览网页时，您可能会觉得网页的文字过小，这时，您可以使用浏览器右下角的缩小、放大按钮进行操作，找到适合阅读的文字大小。二、登录财务综合信息系统登录财务综合信息系统可通过以下两种方式：

1、采用理工大数字校园统一认证平台进行登录认证在跳转过程中可能因数字证书没有安装原因，您的浏览器可能会报安全证书有问题，请点击“继续浏览此网站”。进入“武汉理工大学统一身份认证平台” 点击进入财务综合服务系统 2、您也可以通过计财处网站（https://www.doczj.com/doc/5815017866.html,/）中

“财务综合服务系统”登录入口”进入点击进入理工电子身份证，输入已注册的校园卡号和密码输入已注册的“理工电子身份”，登录成功后，便可跳转到财务综合服务系统。

注：如需通过外网进行浏览访问，请使用网络中心VPN服务。具体操作可参见：https://www.doczj.com/doc/5815017866.html,/2012web/tzgg/201209/t20120927_85753.htm 三、网上报账系统操作财务综合服务系统包括“网上报账系统”、“薪酬发放管理系

网上报销管理系统方案

网上报销管理系统 1.1 业务说明此部分主要包括借款、通用经费报销、差旅费报销用于完成借款、出差以及其他支出（通用经费报销）的报销业务。 1、业务人员如果需要完成日常借款和报销业务，需要在系统内根据类别填写对应单据来进行报销。 2、业务人员只能选择自己负责或经手的项目。 3、借款和报销的审核流程如下： 4、借款和报销线下审批流程和使用纸质单据报销时相同，申请人填写完电子单据后，需要进行打印并按单位制度要求签字，此时电子单据将会传递到财务审核岗位。

5、签字完成后，提交财务，此时财务将对单据进行审核，核实单据是否符合借款和报销要求。 1.2 操作说明 1.2.1 借款登录系统后点击【财务报销系统】-【借款】菜单，如图：操作步骤说明： 1、填写借款事由。 2、项目选择。点击项目文本框右侧的按钮，系统弹出项目选择窗体，如果被选中的项目存在一条预算，预算金额、可用余额会被自动带出，如果选中项目存在多条预算，申请人需要确认此次使用那一条预算。 3、借款类型选择。 4、借款方式选择。借款方式分为现金、支票或转账，选择不同

的方式结算信息中的信息会进行切换。如果选择支票或转账还需填写支票及汇款的具体信息，如图： 5、借款金额必须小于等于可用预算额。 6、填写完成后，点击保存按钮，如存在必填项未填写、申请超出预算、借款类型与申请不匹配等情况，系统会给出相应提示。 7、保存成功后，点击提交审核，借款单即填写完成并提交财务审核岗位审核。 8、如果填写人发现单据填写错误，在财务未进行审核操作之前，

报销人可以在界面中看到“收回”按钮，点击按钮后对单据进行修改。 10、审核没有通过的单据会被退回，填写人会在待办工作中查看到相关单据，相关单据将会在我的单据中显示为红色，如图： 11、申请人根据单位制度要求打印单据并签字，完成后提交相关单据到财务进行审核。 12、借款人可以在【财务报销系统】-【我的单据】以及【个人查询】中的【借款情况】中对本人的借款情况进行查询，如图：

文档之家

Proving correctness of Timed Concurrent Constraint Programs

如何写先进个人事迹

机票预订管理规定

报销系统使用说明

费用报销系统操作手册-流程新建

最新小学生个人读书事迹简介怎么写800字

机票分哪几种

金蝶费用预算及报销系统操作手册-财务操作手册V2.1

机票预订管理规定

个人先进事迹简介

机票管理规定(精编文档).doc

(财务报销管理)财务网上报销系统用户使用手册(V版)

网上报销操作手册(3.0 版)

公司员工订购机票管理规定

优秀党务工作者事迹简介范文

中国石油财务网上报销系统用户使用手册范本

主要事迹简介怎么写(2020年最新)

机票知识(各种退改签以及营运规定)

武汉理工大学网上报账指南

网上报销管理系统方案

最新树立榜样的个人事迹简介怎么写800字