Using Temporal Logic to Specify
Adaptive Program Semantics?
Ji Zhang and Betty H.C.Cheng
Software Engineering and Network Systems Laboratory
Department of Computer Science and Engineering
Michigan State University
East Lansing,Michigan48824
tted
:{zh
1Introduction
Increasingly,computer software must adapt to changing conditions in both the supporting computing and communication infrastructure,as well as in the surrounding physical environment(1).However,adaptive programs may be prone to errant behavior due to its innate high complexity and possibly im-precise requirements.The bene?t expected from adaptations,such as higher reliability and higher availability,may be countered by the errors introduced during the adaptive software development process.Furthermore,the correct-ness of adaptation becomes most crucial when the adaptive software is applied in a safety-critical domain,such as the control software for medical devices, etc.Correctness of adaptive programs cannot be properly addressed without precisely specifying the requirements for the adaptive programs.This paper introduces speci?cations for three commonly used adaptation semantics and two composition techniques to be used for constructing the temporal logic speci?cation of an adaptive program.
Numerous techniques have been proposed to address the correctness of adap-tations.Kulkarni et al.(2)introduced a transitional-invariant lattice approach that uses theorem proving techniques to show that during and after an adapta-tion,the adaptive program is always in correct states with respect to satisfying the transitional-invariants.Some approaches(3;4;5)use formal languages to describe the structural changes of the software at the design and implemen-tation levels.Other approaches(6;7;8;9;10;11;12;13)design adaptation protocols or algorithms to be used during component replacement to achieve a rigorous and safe adaptation procedure.Di?erent approaches assume di?erent adaptation semantics.For example,Appavoo et al.(12)introduced a hot-swapping technique,which does not allow the old and the new components to execute simultaneously to achieve strict sequential semantics.In contrast,in order to improve performance,Chen et al.(11)proposed a graceful adaptation process,which allows the old component and the new component to overlap their executions.These di?erent semantics are implied by their designs and implementations.All of the above techniques focus on the design and the im-plementation of achieving adaptability,while the requirements for adaptation are largely assumed or ambiguous.
We believe that the semantics for adaptive software should be explicitly cap-tured at the requirements level(14).The correctness of adaptive software can then be evaluated with respect to its adaptation requirements speci?cation.
A recent survey(15)describes numerous research e?orts that have proposed ways to formally specify dynamically adaptive programs in the past several years.Graph-based approaches model the dynamic architectures of adaptive programs as graph transformations(16;17;18).Architecture Description Lan-guage(ADL)-based approaches model adaptive programs with connection and
reconnection of connectors(10;19;4).A few e?orts have formally speci?ed the behavioral changes of adaptive programs,including those that use process algebras to specify the behavior of adaptive programs(20;21;22).
This paper focuses on the speci?cation of requirements of adaptations with temporal logics.We model an adaptive program as the composition of a?nite number of steady-state programs(20)(brie?y programs)and the adaptations among these programs.We assume that the properties(e.g.liveness and safety properties)of each program have already been speci?ed with a Linear Tempo-ral Logic(LTL)formula(23).To specify an adaptation from one program to another,we introduce the Adapt operator-extended LTL(A-LTL),an extension to LTL.We introduce three basic adaptation semantics and use A-LTL to for-mally specify their semantics.We can compose the basic adaptation semantics with two types of compositional procedures:neighborhood compositions and sequential compositions to derive more complex adaptation semantics.We introduce adaptation semantics graphs,a graph-based representation of adap-tive programs semantics,which can be automatically processed to generate adaptive program speci?cations.
The formal speci?cations for adaptive programs precisely describe the objec-tives for adaptive programs,which facilitate rigorous software requirements speci?cations,and thus improves the assurance of the software.The adap-tation semantics graphs and the generated temporal logic speci?cations may serve as guidance for the adaptation developers to clarify the intent for the adaptive program.The temporal speci?cations also enable us to perform nu-merous automated analyses of the adaptive program,such as speci?cation consistency,model checking to verify the correctness of a program model, dynamic insertion of adaptation logic code into the program,etc.
We have successfully applied our speci?cation technique to a number of adap-tive mobile computing applications,including MetaSockets(24).The remain-der of this paper is organized as follows.In Section2,we introduce A-LTL and describe three basic adaptation semantics.Section3describes neighborhood speci?cation compositions,sequential speci?cation compositions,and adapta-tion semantics graphs.Section4illustrates our approach with a MetaSockets example.Section5concludes the paper and discusses future directions.
2Adaptation Semantics
In this paper,we take a most general view of programs,i.e.,all programs and adaptive programs are considered as state machines(FSAs).An adaptive program changes its behavior during its execution.The state space describing each di?erent kind of steady-state(20)behavior is a non-adaptive program,or
brie?y a program.The state space describing the change of behavior from one program(source program)to another(target program)is a simple adaptive program,which can be identi?ed by the source and target program pair.
2.1Adapt Operator-Extended LTL
LTL is a temporal extension to propositional logic(23).An LTL formula is constructed over a set of atomic propositions(Π),using?(not)and∧(and) boolean operators,and (next)and U(until)temporal connectives.Other operators are de?ned as abbreviations over the above basic operators,such as ∨(or),→(imply),?(co-imply),?(eventually),2(always),etc.
Existing LTL operators are insu?cient for specifying adaptation behavior. In LTL,the operator closest to capturing the meaning of adaptation is the until(U)operator.However,we cannot express an adaptation from the be-havior speci?ed withφto the behavior speci?ed withψusingφUψfor the following reason:If a state sequenceσ=s0,s1,···satis?esφUψ(denoted as σ|=φUψ),thenφshould hold for all su?xes ofσstarting from all the states before a certain state.However,adaptation semantics usually only requireφto hold for a given interval ofσ.Several temporal logics,including the choppy logic(25),the Propositional Interval Temporal Logic(PITL)(26;27;28;29;
30),and the Interval Temporal Logic(ITL)(31),are capable of expressing adaptation behavior.However,these logics are both too complex and incon-venient for our adaptation speci?cation purposes.By“inconvenient”we mean that they do not have direct notation support.
To specify adaptation behavior,we extend LTL with the adapt operator (“? ”).Informally,a program satis?es“φ? ψ”(φ,ψ,and?are three tem-poral logic formulae)means that the program initially satis?esφ.In a certain state A,it stops being constrained byφ,and in the next state B,it starts to satisfyψ.We formally de?ne A-LTL as follows:
?Ifφis an LTL formula,thenφis also an A-LTL formula.
?Ifφandψare both A-LTL formulae,thenξ=φ? ψis an A-LTL formula.?Ifφandψare both A-LTL formulae,then?φ,φ∧ψ,φ∨ψ,andφUψare all A-LTL formulae.
We de?ne the A-LTL semantics as follows.
?Ifσis an in?nite state sequence andφis an LTL formula,thenσsatis?es φin A-LTL if and only ifσsatis?esφin LTL.Formally,σ|=φi?σ|=φin LTL.
?Ifσis a?nite state sequence andφis an A-LTL formula,thenσ|=fφi?σ |=φ,whereσ is an in?nite state sequence constructed by repeating the
last state ofσ.
?σ|=φ? ψi?there exist a?nite state sequenceσ =(s0,s1,···s k)and an in?nite state sequenceσ =(s k+1,s k+2,···),such thatσ=σ σ ,σ |=fφ,σ |=ψ,and(s k,s k+1)|=f?,whereφ,ψ,and?are A-LTL formulae.
A sequence satisfyingφ? ψcan be considered the concatenation of two subsequences,where the?rst subsequence satis?esφ,the second subse-quence satis?esψ,and the two states connecting the two subsequences satisfy?.
?Other operators(→,∧,∨,U,?,etc)are de?ned similarly as those used in LTL.
The?notation of an adapt operator can be used for specifying additional safe conditions for the state in which the adaptation occurs and logical connections between the behavior before and after adaptation.Although in some cases, the extra constraints are not used(where we simply set?to be true),we ?nd this notation to be useful in many other cases.For example,we can use?=bu?er-empty to constrain that the bu?er must be empty when the adaptation occurs.
We separate the behavior of an adaptive program into adaptation invariants, the properties that hold continuously during an execution of the program,and adaptation variants,the properties that change during the program’s execu-tion.We?rst introduce three adaptation semantics speci?cations in A-LTL. These semantics are used to specify the adaptation variants of adaptations from a given source program to a given target program.Then we introduce composition techniques to handle general adaptive programs.Finally,we com-pose adaptation invariants with adaptation variants to specify the overall adaptive program behavior.
2.2Semantics for Adaptation Variants
Several questions have to be answered before designing an adaptive program: (1)What is the expected behavior after adaptation?(2)What constraints,if any,exist for adaptations to occur?(3)Are the source program behavior and the target program behavior allowed to overlap?(4)Should the source/target program behavior be restricted during an adaptation,and what are the re-strictions,if any?An adaptation speci?cation should precisely address all of the above questions.Based on results presented in the literature and our own experience,we summarize three commonly used semantics for adaptation.By formally specifying these semantics,we are able to precisely answer the above questions.
We assume the source program and the target program have both been spec-i?ed in LTL,named base speci?cations.We specify the adaptation from the source program to the target program with A-LTL by extending the base speci?cations of the source and the target programs.For some adaptations, the source/target program behavior may need to be constrained during the adaptation.These constraints,termed restriction conditions,are speci?ed in LTL.
We assume the adaptive program has moderate computational re?ection(32) capability,i.e.,it is conscious about its adaptation and the currently running steady-state program.This capability can be achieved by simply introducing ?ag propositions in the program to identify its current steady-state program or adaptation status.We assume that a decision-making procedure that trans-lates environment changes into speci?c adaptation requests is available.Our speci?cation technique describes the expected program behavior in response to these requests.We use an atomic proposition A REQ to indicate the receipt of an adaptation request to a target program from the decision making procedure. In this section,we summarize three commonly occurring basic adaptation se-mantics interpretations from the literature(12;11;6;8)speci?ed in terms of A-LTL.There are potentially many other possible adaptation semantics. In all three adaptation speci?cation semantics,we denote the source and the target program base speci?cations as S SPEC and T SPEC,respectively.If appli-cable,the restriction condition during adaptation is R COND.We assume the ?ag propositions are already parts of the speci?cations.We use the term safe states to indicate the states where all the obligations of the source program are ful?lled,thus making it safe to terminate the source behavior.
2.2.1One-point adaptation.
Under one-point adaptation semantics,after receiving an adaptation request
A REQ,the program adapts to the target program T SPEC at a certain point
during its execution.The prerequisite for one-point adaptation is that the source program S SPEC should always eventually reach a safe state during its execution.
(S SPEC∧?A REQ)? T SPEC(1) The formula states that the program initially satis?es S SPEC.After receiving an adaptation request,A REQ,it waits until the program reaches a safe state, i.e.,all obligations generated by S SPEC are satis?ed.Then the program stops being obligated to satisfy S SPEC and starts to satisfy T SPEC.This semantics is
visually presented in Figure1(a),where circles represent a sequence of states. Solid lines represent state intervals and the label of each solid line represents the property that is held by the interval.The arrow points to the states when an adaptation request is received.This semantics is straightforward and is ex-plicitly or implicitly applied by many approaches(e.g.,(12;11;6))to deal with simple cases that do not require restraining the source behavior or overlapping the source and the target behavior.
2.2.2Guided adaptation.
Under guided adaptation semantics(visually depicted in Figure1(b)),after receiving an adaptation request,the program?rst restrains its source pro-gram behavior by a restriction condition,R COND,and then adapts to the target program when it reaches a safe state.This semantics is suitable for adapta-tions whose source programs do not guarantee reaching a safe state within a given amount of time.The restriction condition should ensure that the source program will?nally reach a safe state.
S SPEC∧(?A REQ?1 R COND) ?2 T SPEC(2) This formula states that initially S SPEC is satis?ed.After an adaptation re-quest,A REQ,is received,the program should satisfy a restriction condition
R
COND(marked with?1 ).When the program reaches a safe state of the source,
the program stops being constrained by S SPEC,and starts to satisfy T SPEC (marked with?2 ).The hot-swapping technique introduced by Appavoo et al(12)and the safe adaptation protocol(6)introduced in our previous work use the guided adaptation semantics.
2.2.3Overlap adaptation.
Under overlap adaptation semantics(visually depicted in Figure1(c)),the tar-get program behavior starts before the source program behavior stops.During the overlap of the source and the target behavior,a restriction condition is applied to safeguard the correct behavior of the program.This adaptation se-mantics is appropriate for the case when continuous service from the adaptive program is required.The restriction condition should ensure that the source program reaches a safe state.
S SPEC∧(?A REQ?1 R COND) ?2 true ∧ ?A REQ?1 T SPEC∧(R COND?2 true) (3)
This formula states that initially S SPEC is satis?ed.After an adaptation re-
quest,A REQ ,is received,the program should start to satisfy T SPEC and also
satisfy a restriction condition,R COND (marked with ?1 ).When the program
reaches a safe state of the source program,the program stops being obliged by S SPEC and R COND (marked with ?2 ).The graceful adaptation protocol in-
troduced by Chen et al (11)and the distributed reset protocol introduced by Kulkarni et al (8)use the overlap adaptation
semantics.
SPEC S SPEC
T
SPEC S SPEC
T REQ
R
SPEC S SPEC
T
REQ
COND
Fig.1.Adaptation semantics
2.2.4Safety and Liveness Properties.
Temporal logics are often applied to the speci?cations of safety and liveness properties of a program.A safety property asserts something bad never hap-pens,while a liveness property asserts something good will eventually hap-pen (33).Although general forms of safety and liveness properties are not preserved by the adaptation semantics de?ned above,some common forms of safety and liveness properties are preserved.
We de?ne a formula to be a point safety property if and only if =2?η(read as ηnever holds during execution),where ηis a point formula (a formula that does not contain temporal operators).We de?ne a formula to be point
liveness property if and only if =2(α→?β)(read as it is always the case that ifαholds at some point,thenβwill eventually hold at a point after that point),where bothαandβare point formulae.
LEMMA1:
All three adaptation semantics preserve point safety properties.That is,if (S SPEC∨T SPEC)→2?η,whereηis a point property,thenξ→2?η,whereξis the adaptation speci?cation based on either semantics.We only provide the proof for the one-point adaptation case.Other cases can be proved similarly.
Proof
Let the adaptation speci?cationξbe(Formula1)
ξ=(S
∧?A REQ)? T SPEC
SPEC
For an arbitrary sequenceσ|=ξ,?σ |=S SPEC∧?A REQ andσ |=T SPEC, andσ=σ σ .Since(S SPEC∨T SPEC)→2?η,σ |=2?η,andσ |=2?η. Therefore,σ|=2?η.
This lemma implies that if a propositional invariant(such as a variable is never greater than a given value)should be held in both the source and the target subprograms,then the invariant is also held by a simple adaptive program under all three adaptation semantics.This conclusion does not apply to general temporal properties.
LEMMA2:
Point liveness properties are preserved by all three adaptation semantics. That is,if(S SPEC∨T SPEC)→2(α→?β),thenξ→2(α→?β),whereξis the adaptation speci?cation based on either semantics.Also,we only provide the proof for the one-point adaptation case.Other cases can be proved similarly.
Proof:
Let the adaptation speci?cationξbe(Formula1)
∧?A REQ)? T SPEC
ξ=(S
SPEC
For an arbitrary sequence s0,s1,···|=ξ,?i,such that s0,s1,···s i|=S SPEC∧?A REQ and s i+1,s i+2,···|=T SPEC.
Since(S SPEC∨T SPEC)→2(α→?β),we have s0,s1,···s i|=2(α→?β),and s i+1,s i+2,···|=2(α→?β).
For an arbitrary state s j,if s j|=α,then we have
?if j≤i,then there exists k(j ?if j>i,then there exists k(j That is,s0,s1,···|=2(α→?β) Therefore,we haveξ→2(α→?β). 3Speci?cation Compositions Thus far,we have described how to specify simple adaptive programs.These speci?cations can be composed to describe multiple adaptation options from a single steady-state program.We can also link a sequence of adaptation spec-i?cations together to describe the behavior of executions with multiple adap-tation occurrences. 3.1Neighborhood Composition A simple adaptive program starts from one program and may adapt to only one target program.A more complex adaptive program may adapt to di?erent target programs in response to di?erent adaptation requests.The neighborhood composition is proposed to specify multiple adaptation options from a single program.We de?ne the neighborhood adaptive program of a program S to be the composition of all the simple adaptive programs that share the same source program S.An execution starting from S can either adapt to a target program if a corresponding adaptation request is received,or remain in S if no adaptation request is received.Assume for all target programs,the properties of the simple adaptive program from S to the i th target program T i is speci?ed with an A-LTL formula STi SPEC,and the properties of S are speci?ed with S SPEC.We can construct the speci?cation for the neighborhood of S by the disjunction of S SPEC and STi SPEC.Let N SPEC be the neighborhood speci?cation of S,we have N SPEC=k i=1 STi SPEC∨ S SPEC(4) where k is the number of simple adaptive programs sharing the same source program S. 3.2Sequential Composition A complex adaptive program may sequentially perform adaptations more than once during a single execution.For example,an adaptive program may start from a program A,then sequentially perform adaptations from A to B to obtain program B,and B to C to obtain program C.Assume the properties of A,B,and C are speci?ed with A SPEC,B SPEC,and C SPEC,respectively.The A to B adaptation speci?cation under a given adaptation semantics is a function of A SPEC and B SPEC:AB SPEC=ADAPT1(A SPEC,B SPEC).The B to C adaptation speci?cation under a given adaptation semantics is a function of B SPEC and C SPEC:BC SPEC=ADAPT2(B SPEC,C SPEC).The speci?cation of A to B to C may be constructed by substituting AB SPEC for the B SPEC in BC SPEC. ABC SPEC =ADAPT2(ADAPT1(A SPEC,B SPEC),C SPEC)(5) Similarly,a?nite number of simple adaptive program speci?cations can be sequentially composed to construct the speci?cation of more complex adaptive programs. THEOREM: Both point safety and point liveness properties are preserved by the adap-tation semantics and the two types of compositions. Proof outline: This theorem can be proved by applying Lemma1and Lemma2.?For neighborhood compositions,from the lemmas,we know that if all base speci?cations imply a point safety(liveness)propertyφ,then all the disjuncts implyφas well.Then the disjunction(the neighborhood composition)also impliesφ. ?For sequential composition,we can prove the conclusion inductively. (1)The base case states0-step sequential composition preserves point safety and liveness properties.This has been proved by Lemma1 and Lemma2. (2)Then we assume any n-step sequential composition preserves point safety and liveness properties. An n+1-step sequential composition can be considered as an n-step sequential composition composed with a base speci?cation.Then we can apply Lemma1and Lemma2to the n-step adaptation compo- sition case and claim that all n+1-step sequential compositions also preserve point safety and liveness properties. 3.3Adaptation Invariants In spite of adaptations of a program,some properties should be held true throughout its execution.This type of properties,such as safety and liveness properties,are adaptation invariants.We use LTL formulae to specify adap-tation invariants of the program to ensure the properties that should be held throughout the execution of an adaptive program. 3.4Adaptation Speci?cation Visualization and Automatic Generation An adaptive program can be visually represented as a graph,where programs are vertices and adaptations are arcs.We add temporal logic information to the graph so that we are able to derive the adaptation temporal logic speci?cation automatically from the graph. We de?ne an adaptation semantics graph to be a tuple (S,S0,A,P,Φ,Ψ,INV),where S is a set of vertices representing the set of programs in an adaptive program.S0?S is a set of initial vertices,repre-senting the initial programs of the adaptive program.FunctionΦ:S→LTL maps each program to the base speci?cation for the program.A?S×S is a set of arcs representing adaptations.Function P:A→semantics name maps an adaptation to one of the semantics names{one-point,guided,overlap}.Ψ:A→LTL is a partial function that maps guided or overlap adaptation to their associated restriction conditions.INV is the set of adaptation invariants. The adaptation speci?cations can be derived from the adaptation semantics graph.We have implemented a prototype,ASpecGen,which uses simple edge traversal to automate this process.The complexity of the algorithm is linear to the number of adaptations. 4Case Study In this section we use MetaSockets(24)as an illustrative example to demon-strate our adaptation speci?cation approach.MetaSockets are constructed from the regular Java Socket and MulticastSocket classes;however,their inter-nal structure and behavior can be modi?ed at run time in response to external conditions.MetaSocket behavior can be adapted through the insertion and removal of?lters that manipulate the data stream.For example,?lters can perform encryption,decryption,forward error correction,compression,and so forth. We consider a sender’s MetaSocket with three di?erent?lters:a data com-pression?lter(COM),a DES64-bit encryption?lter(DES64),and a DES 128-bit encryption?lter(DES128).The available adaptations are data com-pression?lter insertion and removal,and DES?lter replacement.Note that to enforce security,the DES?lters can only be replaced by other DES?lters, but cannot be removed.These?lters can be combined in four di?erent con?g-urations:DES64,DES128,DES64with COM(DES64COM),and DES128with COM(DES128COM).We consider the MetaSocket under each con?guration a program.The adaptive program is initially running in the DES64program. 4.1MetaSocket Speci?cations The speci?cations of the programs are described as follows: ?DES64program: DES64 SPEC =(2DES64 FL )∧2(DES64Input(x)→?DES64Output(x)) The DES64Input(DES64Output)are events indicating the input(output) of a packet to(from)the MetaSocket under DES64con?guration.1The ?ag proposition DES64 FL indicates that the program is running under the DES64con?guration.The formula states that under this con?guration,for every input packet to be encoded by the DES64?lter,the MetaSocket should eventually output a DES64encoded packet.The following program aspects can be interpreted in a similar way. ?DES128program: DES128 SPEC =(2DES128FL)∧(2(DES128Input(x)→?DES128Output(x)))?DES64COM program: DES64COM SPEC = (2DES64COM FL )∧(2(DES64COMInput(x)→?DES64COMOutput(x))) ?DES128COM program: = DES128COM SPEC (2DES128COM FL)∧(2(DES128COMInput(x)→?DES128COMOutput(x))) To determine the semantics of each adaptation,we consider the following factors:(1)The MetaSocket component is designed for the transmission of real-time video and audio data.Therefore,we should minimize data blocking. (2)We should not allow both the source and the target programs to input simultaneously because that will cause ambiguity in the input.(3)We should not allow the target program to output data before any output is produced from the source program,otherwise,it will complicate the logic on the receiver. Based on the above considerations,it is appropriate to apply the overlap semantics with conditions prohibiting the types of overlap discussed above. 2. The adaptation semantics graph is visually presented in Figure Fig.2.Visual representation of MetaSocket adaptation semantics graph We use the DES64to DES128adaptation as an example to demonstrate the simple adaptive program speci?cation construction.In order to use overlap semantics,we have to de?ne restriction conditions to prevent overlap of the source and target programs input and the overlap of the source and target programs output.Therefore,we de?ne the restriction conditions to be R (DES64-DES128)=2(?DES64Input(x)∧?DES128Output(x)).(6) COND The intuition for this restriction condition is that it should not accept any more DES64inputs and will not produce any DES128outputs until all DES64out-puts have been produced.Given the source and target program speci?cations, the overlap semantics,and the restriction condition,we apply Formula3to derive the following speci?cation: DES64-DES128 SPEC =(7) DES64SPEC∧ ?A REQ(DES128)true R COND(DES64-DES128) true true ∧ A REQ(DES128)true DES128SPEC∧(R COND(DES64-DES128)true true) Formula(7)states that after the program receives an adaptation request to the DES128program(A REQ(DES128)),it should adapt to the DES128program. Furthermore,the behavior of DES64and DES128may overlap,and during the overlapping period,the program should satisfy the restriction condition R COND(DES64-DES128).In this example,the?notation of the adaptation operators are not used.We simply assign true to?in the four adapt operator locations.With the same approach,we specify other simple adaptive programs in the adaptive program.Further,both the source and the target speci?cations are point liveness properties.We can unify them with the following formula by disregarding the type of inputs and outputs. 2(Input(x)→?Output(x))(8) According to Lemma2,we can conclude that the adaptation also satis?es the point liveness property. In addition to the speci?cation for adaptation behavior,the program should also satisfy a set of adaptation invariants to maintain its integrity.?Security invariant :During program execution,the sender MetaSocket should not cause any loss of packets,i.e.,all input packets should be output: INV2=2(Input(x)→?Output(x)) Note,this invariant is already guaranteed by the point liveness preservation property of the adaptation semantics.(Formula8.) ?Precedence invariant temporal logic(PITL)(26;27;28;29;30),and the interval temporal logic (ITL)(31),are also su?cient to specify adaptation behavior.However,they are generally too complex,and therefore su?er from non-elementary complexity in their decision procedure(25;26;27;28).We?nd the A-LTL to be simple and su?ciently e?ective to specify adaptation behavior,given that the logic was designed to support adaptation explicitly. We have developed an A-LTL model checking algorithm under the assump-tion that the formulae on the two sides of an adapt operator are distinguished by a proposition.This assumption is ensured by the?ag propositions in our speci?cation technique.Our procedure is a variant of the automata-theoretic model checking algorithm introduced by Vardi et al(38;39;40)and Bow-man and Thompson(27;28).The model checking algorithm has complexity exponential to the length of the formula and linear to the size of the program. Note that LTL model checking is in the same complexity class,and A-LTL is a superset of LTL.Therefore,it is unlikely for us to?nd a polynomial model checking algorithm.We are currently investigating optimization techniques, such as on-the-?y model checking proposed by Gerth et al(38). Our future work includes automatically generating program models and code based on a given adaptation semantics,as well as developing e?cient model checking tools to verify the correctness of adaptive programs. References [1]P.K.McKinley,S.M.Sadjadi,E.P.Kasten,B.H.C.Cheng,Composing adaptive software,IEEE Computer37(7)(2004)56–64. [2]S.Kulkarni,K.Biyani,Correctness of component-based adaptation,in: Proceedings of International Symposium on Component-based Software Engineering,2004. [3]https://www.doczj.com/doc/0e16034305.html,ner,J.Parrow,D.Walker,A calculus of mobile processes,I,Infor- mation and Computation100(1)(1992)1–40. [4]J.Kramer,J.Magee,M.Sloman,Con?guring distributed systems,in: Proceedings of the5th workshop on ACM SIGOPS European workshop, ACM Press,1992,pp.1–5. [5] C.E.Cuesta,P.de la Fuente,M.Barrio-Sol′a rzano,Dynamic coordination architecture through the use of re?ection,in:Proceedings of the2001 ACM symposium on Applied computing,ACM Press,2001,pp.134–140. [6]J.Zhang,Z.Yang,B.H.Cheng,P.K.McKinley,Adding safeness to dynamic adaptation techniques,in:Proceedings of ICSE2004Workshop on Architecting Dependable Systems,Edinburgh,Scotland,UK,2004. [7]J.Zhang,B.H.Cheng,Z.Yang,P.K.McKinley,Enabling safe dynamic component-based software adaptation,Architecting Dependable Systems, Lecture Notes in Computer Science,Spring-Verlag,2005. [8]S.S.Kulkarni,K.N.Biyani,U.Arumugam,Composing distributed fault- tolerance components,in:Proccedings of the International Conference on Dependable Systems and Networks(DSN),Supplemental Volume,Work-shop on Principles of Dependable Systems,2003,pp.W127–W136. [9]J.Kramer,J.Magee,The evolving philosophers problem:Dynamic change management,IEEE Trans.Softw.Eng.16(11)(1990)1293–1306. [10]P.Oreizy,N.Medvidovic,R.N.Taylor,Architecture-based runtime soft- ware evolution,in:Proceedings of the20th international conference on Software engineering,IEEE Computer Society,1998,pp.177–186. [11]W.-K.Chen,M.A.Hiltunen,R.D.Schlichting,Constructing adaptive software in distributed systems,in:Proc.of the21st International Con-ference on Distributed Computing Systems,Mesa,AZ,2001. [12]J.Appavoo,K.Hui,C.A.N.Soules,et al.,Enabling autonomic behavior in systems software with hot swapping,IBM System Journal42(1)(2003) 60. [13]N.Amano,T.Watanabe,A software model for?exible and safe adapta- tion of mobile code programs,in:Proceedings of the international work-shop on Principles of software evolution,ACM Press,2002,pp.57–61. [14]D.M.Berry,B.H.Cheng,J.Zhang,The four levels of requirements en- gineering for and in dynamic adaptive systems,in:Proc.of11th Interna-tional Workshop on Requirements Engineering:Foundation for Software Quality,Porto,Portugal,2005. [15]J.Bradbury,J.Cordy,J.Dingel,M.Wermelinger,A survey of self man- agement in dynamic software architecture speci?cations,in:Proc.of the ACM SIGSOFT International Workshop on Self-Managed Systems (WOSS’04),Newport Beach,California,2004,pp.28–33. [16]D.L.M′e tayer,Software architecture styles as graph grammars,in:Pro- ceedings of the4th ACM SIGSOFT symposium on Foundations of soft-ware engineering,ACM Press,1996,pp.15–23. [17]G.Taentzer,M.Goedicke,T.Meyer,Dynamic change management by distributed graph transformation:Towards con?gurable distributed sys-tems,in:Selected papers from the6th International Workshop on Theory and Application of Graph Transformations,Springer-Verlag,2000,pp. 179–193. [18]D.Hirsch,P.Inverardi,U.Montanari,Graph grammars and constraint solving for software architecture styles,in:Proceedings of the third inter-national workshop on Software architecture,ACM Press,1998,pp.69–72. [19]R.N.Taylor,N.Medvidovic,K.M.Anderson,E.J.Whitehead,Jr., J.E.Robbins,A component-and message-based architectural style for GUI software,in:Proceedings of the17th international conference on Software engineering,ACM Press,1995,pp.295–304. [20]R.Allen,R.Douence,D.Garlan,Specifying and analyzing dynamic soft- ware architectures,in:Proceedings of the1998Conference on Funda-mental Approaches to Software Engineering(FASE’98),Lisbon,Portugal, 1998. [21]J.Kramer,J.Magee,Analysing dynamic change in software architec- tures:a case study,in:Proc.of4th IEEE international conference on con?guratble distributed systems,Annapolis,1998. [22]C.Canal,E.Pimentel,J.M.Troya,Speci?cation and re?nement of dy- namic software architectures,in:Proceedings of the TC2First Work-ing IFIP Conference on Software Architecture(WICSA1),Kluwer,B.V., 1999,pp.107–126. [23]A.Pnueli,The temporal logic of programs,in:Proceedings of the18th IEEE Symposium on Foundations of Computer Science,1977,pp.46–57. [24]S.M.Sadjadi,P.K.McKinley,E.P.Kasten,Architecture and operation of an adaptable communication substrate,in:Proceedings of the Ninth IEEE International Workshop on Future Trends of Distributed Comput-ing Systems(FTDCS’03),San Juan,Puerto Rico,2003,pp.46–55. URL ftp://https://www.doczj.com/doc/0e16034305.html,/pub/crg/PAPERS/ftdcs-03.pdf [25]R.Rosner,A.Pnueli,A choppy logic,in:1st IEEE Symposium on Logic in Computer Science,1986,pp.306–313. [26]R.Gomez,H.Bowman,PITL2MONA:Implementing a decision proce- dure for propositional interval temporal logic,Journal of Applied Non-Classical Logics14(1-2)(2004)105–148. URL https://www.doczj.com/doc/0e16034305.html,/pubs/2004/1891 [27]H.Bowman,S.Thompson,A tableau method for Interval Temporal Logic,Technical Report12-97,Computing Laboratory,University of Kent (November1997). URL https://www.doczj.com/doc/0e16034305.html,/pubs/1997/461 [28]H.Bowman,S.J.Thompson,A tableaux method for Interval Temporal Logic with projection,in:TABLEAUX’98,International Conference on Analytic Tableaux and Related Methods,no.1397in Lecture Notes in AI,Springer-Verlag,1998,pp.108–123. URL https://www.doczj.com/doc/0e16034305.html,/pubs/1998/528 [29]B.Moszkowski,A hierarchical completeness proof for Propositional In- terval Temporal Logic with?nite time,Journal of Applied Non-Classical Logics14(1–2)(2004)55–104,special issue on Interval Temporal Logics and Duration Calculi. [30]B.Moszkowski,A hierarchical analysis of propositional temporal logic based on intervals,in:S.Artemov,H.Barringer,A.S.d’Avila Garcez, https://www.doczj.com/doc/0e16034305.html,mb,J.Woods(Eds.),We Will Show Them:Essays in Honour of Dov Gabbay,Vol.2,College Publications,2005,pp.371–440. [31]A.Cau,B.Moszkowski,H.Zedan,Interval temporal logic,Internet(Sep 2002). URL https://www.doczj.com/doc/0e16034305.html,/cau/itlhomepage/ [32]P.Maes,Concepts and experiments in computational re?ection,in:Con- ference proceedings on Object-oriented programming systems,languages and applications,ACM Press,1987,pp.147–155. [33]A.P.Sistla,On characterization of safety and liveness properties in tem- poral logic,in:PODC’85:Proceedings of the Fourth Annual ACM Sym- posium on Principles of Distributed Computing,ACM Press,1985,pp. 39–48. [34]M.B.Dwyer,C.S.Pasareanu,Filter-based model checking of partial systems,in:SIGSOFT’98/FSE-6:Proceedings of the6th ACM SIGSOFT International Symposium on Foundations of Software Engineering,ACM Press,1998,pp.189–202. [35]A.G.Ganek,T.A.Corbi,The dawning of the autonomic computing era, IBM System Journal42(1)(2003)5. [36]D.M.Chess,C.Palmer,S.R.White,Security in an autonomic computing environment,IBM System Journal42(1)(2003)107–118. [37]E.M.Dashofy,A.van der Hoek,R.N.Taylor,Towards architecture-based self-healing systems,in:Proceedings of the?rst workshop on Self-healing systems,ACM Press,2002,pp.21–26. [38]R.Gerth,D.Peled,M.Vardi,P.Wolper,Simple on-the-?y automatic veri?cation of linear temporal logic,in:Proceedings of the Fifteenth IFIP WG6.1International Symposium on Protocol Speci?cation,Testing and Veri?cation(PSTV95),Warsaw,Poland,1995. [39]M.Y.Vardi,P.Wolper,An automata-theoretic approach to automatic pro- gram veri?cation,in:Proceedings of the1st Symposium on Logic in Com-puter Science,Cambridge,England,1986,pp.322–331. [40]M.Y.Vardi,P.Wolper,Reasoning about in?nite computations,https://www.doczj.com/doc/0e16034305.html,- put.115(1)(1994)1–37. 商务公文写作目录 一、商务公文的基本知识 二、应把握的事项与原则 三、常用商务公文写作要点 四、常见错误与问题 一、商务公文的基本知识 1、商务公文的概念与意义 商务公文是商业事务中的公务文书，是企业在生产经营管理活动中产生的，按照严格的、既定的生效程序和规范的格式而制定的具有传递信息和记录作用的载体。规范严谨的商务文书，不仅是贯彻企业执行力的重要保障，而且已经成为现代企业管理的基础中不可或缺的内容。商务公文的水平也是反映企业形象的一个窗口，商务公文的写作能力常成为评价员工职业素质的重要尺度之一。 2、商务公文分类：（1）根据形成和作用的商务活动领域，可分为通用公文和专用公文两类（2）根据内容涉及秘密的程度，可分为对外公开、限国内公开、内部使用、秘密、机密、绝密六类（3）根据行文方向，可分为上行文、下行文、平行文三类（4）根据内容的性质，可分为规范性、指导性、公布性、陈述呈请性、商洽性、证明性公文（5）根据处理时限的要求，可分为平件、急件、特急件三类（6）根据来源，在一个部门内部可分为收文、发文两类。 3、常用商务公文： （1）公务信息：包括通知、通报、通告、会议纪要、会议记录等 （2）上下沟通：包括请示、报告、公函、批复、意见等 （3）建规立矩：包括企业各类管理规章制度、决定、命令、任命等； （4）包容大事小情：包括简报、调查报告、计划、总结、述职报告等； （5）对外宣传：礼仪类应用文、领导演讲稿、邀请函等； （6）财经类：经济合同、委托授权书等； （7）其他：电子邮件、便条、单据类（借条、欠条、领条、收条）等。 考虑到在座的主要岗位，本次讲座涉及请示、报告、函、计划、总结、规章制度的写作，重点谈述职报告的写作。 4、商务公文的特点： （1）制作者是商务组织。（2）具有特定效力，用于处理商务。 （3）具有规范的结构和格式，而不像私人文件靠“约定俗成”的格式。商务公文区别于其它文章的主要特点是具有法定效力与规范格式的文件。 5、商务公文的四个构成要素： （1）意图：主观上要达到的目标 (2）结构：有效划分层次和段落，巧设过渡和照应 (3）材料：组织材料要注意多、细、精、严 (4) 正确使用专业术语、熟语、流行语等词语，适当运用模糊语言、模态词语与古词语。 6、基本文体与结构 商务文体区别于其他文体的特殊属性主要有直接应用性、全面真实性、结构格式的规范性。其特征表现为：被强制性规定采用白话文形式，兼用议论、说明、叙述三种基本表达方法。商务公文的基本组成部分有：标题、正文、作者、日期、印章或签署、主题词。其它组成部分有文头、发文字号、签发人、保密等级、紧急程度、主送机关、附件及其标记、抄送机关、注释、印发说明等。印章或签署均为证实公文作者合法性、真实性及公文效力的标志。 7、稿本 （1）草稿。常有“讨论稿”“征求意见稿”“送审稿”“草稿”“初稿”“二稿”“三稿”等标记。（2）定稿。是制作公文正本的标准依据。有法定的生效标志（签发等）。（3）正本。格式正规并有印章或签署等表明真实性、权威性、有效性。（4）试行本。在试验期间具有正式公文的法定效力。（5）暂行本。在规定 关于会议纪要的规范格式和写作要求 一、会议纪要的概念 会议纪要是一种记载和传达会议基本情况或主要精神、议定事项等内容的规定性公文。是在会议记录的基础上，对会议的主要内容及议定的事项，经过摘要整理的、需要贯彻执行或公布于报刊的具有纪实性和指导性的文件。 会议纪要根据适用范围、内容和作用，分为三种类型： 1、办公会议纪要(也指日常行政工作类会议纪要)，主要用于单位开会讨论研究问题，商定决议事项，安排布置工作，为开展工作提供指导和依据。如，xx学校工作会议纪要、部长办公会议纪要、市委常委会议纪要。 2、专项会议纪要(也指协商交流性会议纪要)，主要用于各类交流会、研讨会、座谈会等会议纪要，目的是听取情况、传递信息、研讨问题、启发工作等。如，xx县脱贫致富工作座谈会议纪要。 3、代表会议纪要(也指程序类会议纪要)。它侧重于记录会议议程和通过的决议，以及今后工作的建议。如《××省第一次盲人聋哑人代表会议纪要》、《xx市第x次代表大会会议纪要》。 另外，还有工作汇报、交流会，部门之间的联席会等方面的纪要，但基本上都系日常工作类的会议纪要。 二、会议纪要的格式 会议纪要通常由标题、正文、结尾三部分构成。 1、标题有三种方式：一是会议名称加纪要，如《全国农村工作会议纪要》;二是召开会议的机关加内容加纪要，也可简化为机关加纪要，如《省经贸委关于企业扭亏会议纪要》、《xx组织部部长办公会议纪要》;三是正副标题相结合，如《维护财政制度加强经济管理——在xx部门xx座谈会上的发言纪要》。 会议纪要应在标题的下方标注成文日期，位置居中，并用括号括起。作为文件下发的会议纪要应在版头部分标注文号，行文单位和成文日期在文末落款(加盖印章)。 2、会议纪要正文一般由两部分组成。 (1)开头，主要指会议概况，包括会议时间、地点、名称、主持人，与会人员，基本议程。 (2)主体，主要指会议的精神和议定事项。常务会、办公会、日常工作例会的纪要，一般包括会议内容、议定事项，有的还可概述议定事项的意义。工作会议、专业会议和座谈会的纪要，往往还要写出经验、做法、今后工作的意见、措施和要求。 (3)结尾，主要是对会议的总结、发言评价和主持人的要求或发出的号召、提出的要求等。一般会议纪要不需要写结束语，主体部分写完就结束。 三、会议纪要的写法 根据会议性质、规模、议题等不同，正文部分大致可以有以下几种写法： 1、集中概述法(综合式)。这种写法是把会议的基本情况，讨 titlesec&titletoc中文文档 张海军编译 makeday1984@https://www.doczj.com/doc/0e16034305.html, 2009年10月 目录 1简介,1 2titlesec基本功能,2 2.1.格式,2.—2.2.间隔, 3.—2.3.工具,3. 3titlesec用法进阶,3 3.1.标题格式,3.—3.2.标题间距, 4.—3.3.与间隔相关的工具, 5.—3.4.标题 填充,5.—3.5.页面类型,6.—3.6.断行,6. 4titletoc部分,6 4.1.titletoc快速上手,6. 1简介 The titlesec and titletoc宏包是用来改变L A T E X中默认标题和目录样式的，可以提供当前L A T E X中没有的功能。Piet van Oostrum写的fancyhdr宏包、Rowland McDonnell的sectsty宏包以及Peter Wilson的tocloft宏包用法更容易些；如果希望用法简单的朋友，可以考虑使用它们。 要想正确使用titlesec宏包，首先要明白L A T E X中标题的构成，一个完整的标题是由标签+间隔+标题内容构成的。比如： 1.这是一个标题，此标题中 1.就是这个标题的标签，这是一个标签是此标题的内容，它们之间的间距就是间隔了。 1 2titlesec基本功能 改变标题样式最容易的方法就是用几向个命令和一系列选项。如果你感觉用这种方法已经能满足你的需求，就不要读除本节之外的其它章节了1。 2.1格式 格式里用三组选项来控制字体的簇、大小以及对齐方法。没有必要设置每一个选项，因为有些选项已经有默认值了。 rm s f t t md b f up i t s l s c 用来控制字体的族和形状2，默认是bf,详情见表1。 项目意义备注（相当于） rm roman字体\textrm{...} sf sans serif字体\textsf{...} tt typewriter字体\texttt{...} md mdseries(中等粗体)\textmd{...} bf bfseries(粗体)\textbf{...} up直立字体\textup{...} it italic字体\textit{...} sl slanted字体\textsl{...} sc小号大写字母\textsc{...} 表1:字体族、形状选项 bf和md属于控制字体形状，其余均是切换字体族的。 b i g medium s m a l l t i n y（大、中、小、很小） 用来标题字体的大小，默认是big。 1这句话是宏包作者说的，不过我感觉大多情况下，是不能满足需要的，特别是中文排版，英文 可能会好些！ 2L A T E X中的字体有5种属性：编码、族、形状、系列和尺寸。 2 毕业论文写作要求与格式规范 关于《毕业论文写作要求与格式规范》，是我们特意为大家整理的，希望对大家有所帮助。 (一)文体 毕业论文文体类型一般分为：试验论文、专题论文、调查报告、文献综述、个案评述、计算设计等。学生根据自己的实际情况，可以选择适合的文体写作。 (二)文风 符合科研论文写作的基本要求：科学性、创造性、逻辑性、 实用性、可读性、规范性等。写作态度要严肃认真，论证主题应有一定理论或应用价值;立论应科学正确，论据应充实可靠，结构层次应清晰合理，推理论证应逻辑严密。行文应简练，文笔应通顺，文字应朴实，撰写应规范，要求使用科研论文特有的科学语言。 (三)论文结构与排列顺序 毕业论文，一般由封面、独创性声明及版权授权书、摘要、目录、正文、后记、参考文献、附录等部分组成并按前后顺序排列。 1.封面：毕业论文(设计)封面具体要求如下： (1)论文题目应能概括论文的主要内容，切题、简洁，不超过30字，可分两行排列; (2)层次：大学本科、大学专科 (3)专业名称：机电一体化技术、计算机应用技术、计算机网络技术、数控技术、模具设计与制造、电子信息、电脑艺术设计、会计电算化、商务英语、市场营销、电子商务、生物技术应用、设施农业技术、园林工程技术、中草药栽培技术和畜牧兽医等专业，应按照标准表述填写; (4)日期：毕业论文(设计)完成时间。 2.独创性声明和关于论文使用授权的说明：需要学生本人签字。 3.摘要：论文摘要的字数一般为300字左右。摘要是对论文的内容不加注释和评论的简短陈述，是文章内容的高度概括。主要内容包括：该项研究工作的内容、目的及其重要性;所使用的实验方法;总结研究成果，突出作者的新见解;研究结论及其意义。摘要中不列举例证，不描述研究过程，不做自我评价。 公文格式规范与常见公文写作 一、公文概述与公文格式规范 党政机关公文种类的区分、用途的确定及格式规范等，由中共中央办公厅、国务院办公厅于2012年4月16日印发，2012年7月1日施行的《党政机关公文处理工作条例》规定。之前相关条例、办法停止执行。 （一）公文的含义 公文，即公务文书的简称，属应用文。 广义的公文，指党政机关、社会团体、企事业单位，为处理公务按照一定程序而形成的体式完整的文字材料。 狭义的公文，是指在机关、单位之间，以规范体式运行的文字材料，俗称“红头文件”。 ?（二）公文的行文方向和原则 ?、上行文下级机关向上级机关行文。有“请示”、“报告”、和“意见”。 ?、平行文同级机关或不相隶属机关之间行文。主要有“函”、“议案”和“意见”。 ?、下行文上级机关向下级机关行文。主要有“决议”、“决定”、“命令”、“公报”、“公告”、“通告”、“意见”、“通知”、“通报”、“批复”和“会议纪要”等。 ?其中，“意见”、“会议纪要”可上行文、平行文、下行文。?“通报”可下行文和平行文。 ?原则： ?、根据本机关隶属关系和职权范围确定行文关系 ?、一般不得越级行文 ?、同级机关可以联合行文 ?、受双重领导的机关应分清主送机关和抄送机关 ?、党政机关的部门一般不得向下级党政机关行文 ?(三) 公文的种类及用途 ?、决议。适用于会议讨论通过的重大决策事项。 ?、决定。适用于对重要事项作出决策和部署、奖惩有关单位和人员、变更或撤销下级机关不适当的决定事项。 ?、命令（令）。适用于公布行政法规和规章、宣布施行重大强制性措施、批准授予和晋升衔级、嘉奖有关单位和人员。 ?、公报。适用于公布重要决定或者重大事项。 ?、公告。适用于向国内外宣布重要事项或者法定事项。 ?、通告。适用于在一定范围内公布应当遵守或者周知的事项。?、意见。适用于对重要问题提出见解和处理办法。 ?、通知。适用于发布、传达要求下级机关执行和有关单位周知或者执行的事项，批转、转发公文。 ?、通报。适用于表彰先进、批评错误、传达重要精神和告知重要情况。 ?、报告。适用于向上级机关汇报工作、反映情况，回复上级机关的询问。 ?、请示。适用于向上级机关请求指示、批准。 ?、批复。适用于答复下级机关请示事项。 ?、议案。适用于各级人民政府按照法律程序向同级人民代表大会或者人民代表大会常务委员会提请审议事项。 ?、函。适用于不相隶属机关之间商洽工作、询问和答复问题、请求批准和答复审批事项。 ?、纪要。适用于记载会议主要情况和议定事项。?（四）、公文的格式规范 ?、眉首的规范 ?（）、份号 ?也称编号，置于公文首页左上角第行，顶格标注。“秘密”以上等级的党政机关公文，应当标注份号。 ?（）、密级和保密期限 ?分“绝密”、“机密”、“秘密”三个等级。标注在份号下方。?（）、紧急程度 ?分为“特急”和“加急”。由公文签发人根据实际需要确定使用与否。标注在密级下方。 ?（）、发文机关标志（或称版头） ?由发文机关全称或规范化简称加“文件”二字组成。套红醒目，位于公文首页正中居上位置（按《党政机关公文格式》标准排 ctex宏包说明 https://www.doczj.com/doc/0e16034305.html,? 版本号：v1.02c修改日期：2011/03/11 摘要 ctex宏包提供了一个统一的中文L A T E X文档框架，底层支持CCT、CJK和xeCJK 三种中文L A T E X系统。ctex宏包提供了编写中文L A T E X文档常用的一些宏定义和命令。 ctex宏包需要CCT系统或者CJK宏包或者xeCJK宏包的支持。主要文件包括ctexart.cls、ctexrep.cls、ctexbook.cls和ctex.sty、ctexcap.sty。 ctex宏包由https://www.doczj.com/doc/0e16034305.html,制作并负责维护。 目录 1简介2 2使用帮助3 2.1使用CJK或xeCJK (3) 2.2使用CCT (3) 2.3选项 (4) 2.3.1只能用于文档类的选项 (4) 2.3.2只能用于文档类和ctexcap.sty的选项 (4) 2.3.3中文编码选项 (4) 2.3.4中文字库选项 (5) 2.3.5CCT引擎选项 (5) 2.3.6排版风格选项 (5) 2.3.7宏包兼容选项 (6) 2.3.8缺省选项 (6) 2.4基本命令 (6) 2.4.1字体设置 (6) 2.4.2字号、字距、字宽和缩进 (7) ?https://www.doczj.com/doc/0e16034305.html, 1 1简介2 2.4.3中文数字转换 (7) 2.5高级设置 (8) 2.5.1章节标题设置 (9) 2.5.2部分修改标题格式 (12) 2.5.3附录标题设置 (12) 2.5.4其他标题设置 (13) 2.5.5其他设置 (13) 2.6配置文件 (14) 3版本更新15 4开发人员17 1简介 这个宏包的部分原始代码来自于由王磊编写cjkbook.cls文档类，还有一小部分原始代码来自于吴凌云编写的GB.cap文件。原来的这些工作都是零零碎碎编写的，没有认真、系统的设计，也没有用户文档，非常不利于维护和改进。2003年，吴凌云用doc和docstrip工具重新编写了整个文档，并增加了许多新的功能。2007年，oseen和王越在ctex宏包基础上增加了对UTF-8编码的支持，开发出了ctexutf8宏包。2009年5月，我们在Google Code建立了ctex-kit项目1，对ctex宏包及相关宏包和脚本进行了整合，并加入了对XeT E X的支持。该项目由https://www.doczj.com/doc/0e16034305.html,社区的开发者共同维护，新版本号为v0.9。在开发新版本时，考虑到合作开发和调试的方便，我们不再使用doc和docstrip工具，改为直接编写宏包文件。 最初Knuth设计开发T E X的时候没有考虑到支持多国语言，特别是多字节的中日韩语言。这使得T E X以至后来的L A T E X对中文的支持一直不是很好。即使在CJK解决了中文字符处理的问题以后，中文用户使用L A T E X仍然要面对许多困难。最常见的就是中文化的标题。由于中文习惯和西方语言的不同，使得很难直接使用原有的标题结构来表示中文标题。因此需要对标准L A T E X宏包做较大的修改。此外，还有诸如中文字号的对应关系等等。ctex宏包正是尝试着解决这些问题。中间很多地方用到了在https://www.doczj.com/doc/0e16034305.html,论坛上的讨论结果，在此对参与讨论的朋友们表示感谢。 ctex宏包由五个主要文件构成：ctexart.cls、ctexrep.cls、ctexbook.cls和ctex.sty、ctexcap.sty。ctex.sty主要是提供整合的中文环境，可以配合大多数文档类使用。而ctexcap.sty则是在ctex.sty的基础上对L A T E X的三个标准文档类的格式进行修改以符合中文习惯，该宏包只能配合这三个标准文档类使用。ctexart.cls、ctexrep.cls、ctexbook.cls则是ctex.sty、ctexcap.sty分别和三个标准文档类结合产生的新文档类，除了包含ctex.sty、ctexcap.sty的所有功能，还加入了一些修改文档类缺省设置的内容（如使用五号字体为缺省字体）。 1https://www.doczj.com/doc/0e16034305.html,/p/ctex-kit/ 学生会文档书写格式规范要求 目前各部门在日常文书编撰中大多按照个人习惯进行排版，文档中字体、文字大小、行间距、段落编号、页边距、落款等参数设置不规范，严重影响到文书的标准性和美观性，以下是文书标准格式要求及日常文档书写注意事项，请各部门在今后工作中严格实行： 一、文件要求 1.文字类采用Word格式排版 2.统计表、一览表等表格统一用Excel格式排版 3.打印材料用纸一般采用国际标准A4型（210mm×297mm），左侧装订。版面方向以纵向为主，横向为辅，可根据实际需要确定 4.各部门的职责、制度、申请、请示等应一事一报，禁止一份行文内同时表述两件工作。 5.各类材料标题应规范书写，明确文件主要内容。 二、文件格式 （一）标题 1.文件标题：标题应由发文机关、发文事由、公文种类三部分组成，黑体小二号字,不加粗，居中，段后空1行。 （二）正文格式 1. 正文字体：四号宋体，在文档中插入表格，单元格内字体用宋体，字号可根据内容自行设定。 2.页边距：上下边距为2.54厘米；左右边距为 3.18厘米。 3.页眉、页脚：页眉为1.5厘米；页脚为1.75厘米； 4.行间距：1.5倍行距。 5.每段前的空格请不要使用空格，应该设置首先缩进2字符 6.年月日表示：全部采用阿拉伯数字表示。 7.文字从左至右横写。 （三）层次序号 (1)一级标题：一、二、三、 (2)二级标题：（一）（二）（三） (3)三级标题：1. 2. 3. (4)四级标题：（1）（2）（3） 注：三个级别的标题所用分隔符号不同，一级标题用顿号“、”例如：一、二、等。二级标题用括号不加顿号，例如：（三）（四）等。三级标题用字符圆点“.”例如：5. 6.等。 （四）、关于落款： 1.对外行文必须落款“湖南环境生物专业技术学院学生会”“校学生会”各部门不得随意使用。 2.各部门文件落款需注明组织名称及部门“湖南环境生物专业技术学院学生会XX部”“校学生会XX部” 3.所有行文落款不得出现“环境生物学院”“湘环学院”“学生会”等表述不全的简称。 4.落款填写至文档末尾右对齐，与前一段间隔2行 5.时间落款：文档中落款时间应以“2016年5月12日”阿拉伯数字 政府公文写作格式 一、眉首部分 （一）发文机关标识 平行文和下行文的文件头，发文机关标识上边缘至上页边为62mm，发文机关下边缘至红色反线为28mm。 上行文中，发文机关标识上边缘至版心上边缘为80mm，即与上页边距离为117mm，发文机关下边缘至红色反线为30mm。 发文机关标识使用字体为方正小标宋_GBK，字号不大于22mm×15mm。 （二）份数序号 用阿拉伯数字顶格标识在版心左上角第一行，不能少于2位数。标识为“编号000001” （三）秘密等级和保密期限 用3号黑体字顶格标识在版心右上角第一行，两字中间空一字。如需要加保密期限的，密级与期限间用“★”隔开，密级中则不空字。 （四）紧急程度 用3号黑体字顶格标识在版心右上角第一行，两字中间空一字。如同时标识密级，则标识在右上角第二行。 （五）发文字号 标识在发文机关标识下两行，用3号方正仿宋_GBK字体剧 中排布。年份、序号用阿拉伯数字标识，年份用全称，用六角括号“〔〕”括入。序号不用虚位，不用“第”。发文字号距离红色反线4mm。 （六）签发人 上行文需要标识签发人，平行排列于发文字号右侧，发文字号居左空一字，签发人居右空一字。“签发人”用3号方正仿宋_GBK，后标全角冒号，冒号后用3号方正楷体_GBK标识签发人姓名。多个签发人的，主办单位签发人置于第一行，其他从第二行起排在主办单位签发人下，下移红色反线，最后一个签发人与发文字号在同一行。 二、主体部分 （一）标题 由“发文机关+事由+文种”组成，标识在红色反线下空两行，用2号方正小标宋_GBK，可一行或多行居中排布。 （二）主送机关 在标题下空一行，用3号方正仿宋_GBK字体顶格标识。回行是顶格，最后一个主送机关后面用全角冒号。 （三）正文 主送机关后一行开始，每段段首空两字，回行顶格。公文中的数字、年份用阿拉伯数字，不能回行，阿拉伯数字：用3号Times New Roman。正文用3号方正仿宋_GBK，小标题按照如下排版要求进行排版： tabularx宏包中改变弹性列的宽度\hsize 分类：latex 2012-03-07 21:54 12人阅读评论(0) 收藏编辑删除 \documentclass{article} \usepackage{amsmath} \usepackage{amssymb} \usepackage{latexsym} \usepackage{CJK} \usepackage{tabularx} \usepackage{array} \newcommand{\PreserveBackslash}[1]{\let \temp =\\#1 \let \\ = \temp} \newcolumntype{C}[1]{>{\PreserveBackslash\centering}p{#1}} \newcolumntype{R}[1]{>{\PreserveBackslash\raggedleft}p{#1}} \newcolumntype{L}[1]{>{\PreserveBackslash\raggedright}p{#1}} \begin{document} \begin{CJK*}{GBK}{song} \CJKtilde \begin{tabularx}{10.5cm}{|p{3cm} |>{\setlength{\hsize}{.5\hsize}\centering}X |>{\setlength{\hsize}{1.5\hsize}}X|} %\hsize是自动计算的列宽度，上面{.5\hsize}与{1.5\hsize}中的\hsize前的数字加起来必须等于表格的弹性列数量。对于本例，弹性列有2列，所以“.5+1.5=2”正确。 %共3列，总列宽为10.5cm。第1列列宽为3cm，第3列的列宽是第2列列宽的3倍，其宽度自动计算。第2列文字左右居中对齐。注意：\multicolum命令不能跨越X列。 \hline 聪明的鱼儿在咬钩前常常排祠再三& 这是因为它们要荆断食物是否安全&知果它们认为有危险\\ \hline 它们枕不会吃& 如果它们判定没有危险& 它们就食吞钩\\ \hline 一眼识破诱饵的危险，却又不由自主地去吞钩的& 那才正是人的心理而不是鱼的心理& 是人的愚合而不是鱼的恳奋\\ 广州中医药大学研究生学位论文基本要求与写作规范 为了进一步提高学位工作水平和学位论文质量，保证我校学位论文在结构和格式上的规范与统一，特做如下规定： 一、学位论文基本要求 （一）科学学位硕士论文要求 1.论文的基本科学论点、结论，应在中医药学术上和中医药科学技术上具有一定的理论意义和实践价值。 2.论文所涉及的内容，应反映出作者具有坚实的基础理论和系统的专门知识。 3.实验设计和方法比较先进，并能掌握本研究课题的研究方法和技能。 4.对所研究的课题有新的见解。 5.在导师指导下研究生独立完成。 6.论文字数一般不少于3万字，中、英文摘要1000字左右。 （二）临床专业学位硕士论文要求 临床医学硕士专业学位申请者在临床科研能力训练中学会文献检索、收集资料、数据处理等科学研究的基本方法,培养临床思维能力与分析能力,完成学位论文。 1.学位论文包括病例分析报告及文献综述。 2.学位论文应紧密结合中医临床或中西结合临床实际，以总结临床实践经验为主。 3.学位论文应表明申请人已经掌握临床科学研究的基本方法。 4.论文字数一般不少于15000字，中、英文摘要1000字左右。 （三）科学学位博士论文要求 1.研究的课题应在中医药学术上具有较大的理论意义和实践价值。 2.论文所涉及的内容应反映作者具有坚实宽广的理论基础和系统深入的专门知识，并表明作者具有独立从事科学研究工作的能力。 3.实验设计和方法在国内同类研究中属先进水平，并能独立掌握本研究课题的研究方法和技能。 4.对本研究课题有创造性见解，并取得显著的科研成果。 5.学位论文必须是作者本人独立完成，与他人合作的只能提出本人完成的部分。 6.论文字数不少于5万字，中、英摘要3000字；详细中文摘要(单行本)1万字左右。 （四）临床专业学位博士论文要求 1.要求论文课题紧密结合中医临床或中西结合临床实际，研究结果对临床工作具有一定的应用价值。 2.论文表明研究生具有运用所学知识解决临床实际问题和从事临床科学研究的能力。 3.论文字数一般不少于3万字，中、英文摘要2000字；详细中文摘要(单行本)5000字左右。 二、学位论文的格式要求 （一）学位论文的组成 博士、硕士学位论文一般应由以下几部分组成，依次为：1.论文封面；2. 原创性声明及关于学位论文使用授权的声明；3.中文摘要；4.英文摘要；5.目录； 6.引言； 7.论文正文； 8.结语； 9.参考文献；10.附录；11.致谢。 1.论文封面：采用研究生处统一设计的封面。论文题目应以恰当、简明、引人注目的词语概括论文中最主要的内容。避免使用不常见的缩略词、缩写字，题名一般不超过30个汉字。论文封面“指导教师”栏只写入学当年招生简章注明、经正式遴选的指导教师1人，协助导师名字不得出现在论文封面。 2．原创性声明及关于学位论文使用授权的声明（后附）。 3.中文摘要：要说明研究工作目的、方法、成果和结论。并写出论文关键词3～5个。 4.英文摘要：应有题目、专业名称、研究生姓名和指导教师姓名，内容与中文提要一致，语句要通顺，语法正确。并列出与中文对应的论文关键词3～5个。 5.目录：将论文各组成部分(1～3级)标题依次列出，标题应简明扼要，逐项标明页码，目录各级标题对齐排。 6.引言：在论文正文之前，简要说明研究工作的目的、范围、相关领域前人所做的工作和研究空白，本研究理论基础、研究方法、预期结果和意义。应言简 （公文写作）毕业论文写作要求和格式规范 中国农业大学继续教育学院 毕业论文写作要求和格式规范 壹、写作要求 （壹）文体 毕业论文文体类型壹般分为：试验论文、专题论文、调查方案、文献综述、个案评述、计算设计等。学生根据自己的实际情况，能够选择适合的文体写作。 （二）文风 符合科研论文写作的基本要求：科学性、创造性、逻辑性、实用性、可读性、规范性等。写作态度要严肃认真，论证主题应有壹定理论或应用价值；立论应科学正确，论据应充实可靠，结构层次应清晰合理，推理论证应逻辑严密。行文应简练，文笔应通顺，文字应朴实，撰写应规范，要求使用科研论文特有的科学语言。 （三）论文结构和排列顺序 毕业论文，壹般由封面、独创性声明及版权授权书、摘要、目录、正文、后记、参考文献、附录等部分组成且按前后顺序排列。 1．封面：毕业论文（设计）封面（见文件5）具体要求如下： （1）论文题目应能概括论文的主要内容，切题、简洁，不超过30字，可分俩行排列； （2）层次：高起本，专升本，高起专； （3）专业名称：现开设园林、农林经济管理、会计学、工商管理等专业，应按照标准表述填写； （4）密级：涉密论文注明相应保密年限； （5）日期：毕业论文完成时间。 2．独创性声明和关于论文使用授权的说明：（略）。 3．摘要：论文摘要的字数壹般为300字左右。摘要是对论文的内容不加注释和评论的简短陈述，是文章内容的高度概括。主要内容包括：该项研究工作的内容、目的及其重要性；所使用的实验方法；总结研究成果，突出作者的新见解；研究结论及其意义。摘要中不列举例证，不描述研究过程，不做自我评价。 论文摘要后另起壹行注明本文的关键词，关键词是供检索用的主题词条，应采用能够覆盖论文内容的通用专业术语，符合学科分类，壹般为3～5个，按照词条的外延层次从大到小排列。 4．目录（目录示例见附件3）：独立成页，包括论文中的壹级、二级标题、后记、参考文献、和附录以及各项所于的页码。 5．正文：包括前言、论文主体和结论 前言：为正文第壹部分内容，简单介绍本项研究的背景和国内外研究成果、研究现状，明确研究目的、意义以及要解决的问题。 论文主体：是全文的核心部分，于正文中应将调查、研究中所得的材料和数据加工整理和分析研究，提出论点，突出创新。内容可根据学科特点和研究内容的性质而不同。壹般包括：理论分析、计算方法、实验装置和测试方法、对实验结果或调研结果的分析和讨论，本研究方法和已有研究方法的比较等方面。内容要求论点正确，推理严谨，数据可靠，文字精炼，条理分明，重点突出。 结论：为正文最后壹部分，是对主要成果的归纳和总结，要突出创新点，且以简练的文字对所做的主要工作进行评价。 6．后记：对整个毕业论文工作进行简单的回顾总结，对给予毕业论文工作提供帮助的组织或个人表示感谢。内容应尽量简单明了，壹般为200字左右。 7．参考文献：是论文不可或缺的组成部分。它既可反映毕业论文工作中取材广博程度，又可反映文稿的科学依据和作者尊重他人研究成果的严肃态度，仍能够向读者提供有关 %=== 配合前面的ntheorem宏包产生各种定理结构,重定义一些正文相关标题===% \theoremstyle{plain} \theoremheaderfont{\normalfont\rmfamily\CJKfamily{hei}} \theorembodyfont{\normalfont\rm\CJKfamily{song}} \theoremindent0em \theoremseparator{\hspace{1em}} \theoremnumbering{arabic} %\theoremsymbol{} %定理结束时自动添加的标志 \newtheorem{definition}{\hspace{2em}定义}[chapter] %\newtheorem{definition}{\hei 定义}[section] %!!!注意当section为中国数字时，[sction]不可用！ \newtheorem{proposition}{\hspace{2em}命题}[chapter] \newtheorem{property}{\hspace{2em}性质}[chapter] \newtheorem{lemma}{\hspace{2em}引理}[chapter] %\newtheorem{lemma}[definition]{引理} \newtheorem{theorem}{\hspace{2em}定理}[chapter] \newtheorem{axiom}{\hspace{2em}公理}[chapter] \newtheorem{corollary}{\hspace{2em}推论}[chapter] \newtheorem{exercise}{\hspace{2em}习题}[chapter] \theoremsymbol{$\blacksquare$} \newtheorem{example}{\hspace{2em}例}[chapter] \theoremstyle{nonumberplain} \theoremheaderfont{\CJKfamily{hei}\rmfamily} \theorembodyfont{\normalfont \rm \CJKfamily{song}} \theoremindent0em \theoremseparator{\hspace{1em}} \theoremsymbol{$\blacksquare$} \newtheorem{proof}{\hspace{2em}证明} \usepackage{amsmath}%数学 \usepackage[amsmath,thmmarks,hyperref]{ntheorem} \theoremstyle{break} \newtheorem{example}{Example}[section] 【最新整理，下载后即可编辑】 广东工业大学成人高等教育 本科生毕业论文格式规范（摘录整理） 一、毕业论文完成后应提交的资料 最终提交的毕业论文资料应由以下部分构成： （一）毕业论文任务书（一式两份，与论文正稿装订在一起）（二）毕业论文考核评议表（一式三份，学生填写表头后发电子版给老师） （三）毕业论文答辩记录（一份, 学生填写表头后打印出来，答辩时使用） （四）毕业论文正稿（一式两份，与论文任务书装订在一起），包括以下内容： 1、封面 2、论文任务书 3、中、英文摘要（先中文摘要，后英文摘要，分开两页排版） 4、目录 5、正文（包括：绪论、正文主体、结论） 6、参考文献 7、致谢 8、附录（如果有的话） （五）论文任务书和论文正稿的光盘 二、毕业论文资料的填写与装订 毕业论文须用计算机打印，一律使用A4打印纸，单面打印。 毕业论文任务书、毕业论文考核评议表、毕业论文正稿、答辩纪录纸须用计算机打印，一律使用A4打印纸。答辩提问记录一律用黑色或蓝黑色墨水手写，要求字体工整，卷面整洁；任务书由指导教师填写并签字，经主管院领导签字后发出。 毕业论文使用统一的封面，资料装订顺序为：毕业论文封面、论文任务书、考核评议表、答辩记录、中文摘要、英文摘要、目录、正文、参考文献、致谢、附录（如果有的话）。论文封面要求用A3纸包边。 三、毕业论文撰写的内容与要求 一份完整的毕业论文正稿应包括以下几个方面： （一）封面（见封面模版） （二）论文题目（填写在封面上，题目使用2号隶书，写作格式见封面模版） 题目应简短、明确，主标题不宜超过20字；可以设副标题。（三）论文摘要（写作格式要求见《摘要、绪论、结论、参考文献写作式样》P1～P2） 1、中文“摘要”字体居中，独占一页 使用Groff 生成独立于设备的文档开始之前 了解本教程中包含的内容和如何最好地利用本教程，以及在使用本教程的过程中您需要完成的工作。 关于本教程 本教程提供了使用Groff(GNU Troff)文档准备系统的简介。其中介绍了这个系统的工作原理、如何使用Groff命令语言为其编写输入、以及如何从该输入生成各种格式的独立于设备的排版文档。 本教程所涉及的主题包括： 文档准备过程 输入文件格式 语言语法 基本的格式化操作 生成输出 目标 本教程的主要目标是介绍Groff，一种用于文档准备的开放源码系统。如果您需要在应用程序中构建文档或帮助文件、或为客户和内部使用生成任何类型的打印或屏幕文档(如订单列表、故障单、收据或报表)，那么本教程将向您介绍如何开始使用Groff以实现这些任务。 在学习了本教程之后，您应该完全了解Groff的基本知识，包括如何编写和处理基本的Groff输入文件、以及如何从这些文件生成各种输出。 先决条件 本教程的目标读者是入门级到中级水平的UNIX?开发人员和管理员。您应 该对使用UNIX命令行Shell和文本编辑器有基本的了解。 系统要求 要运行本教程中的示例，您需要访问运行UNIX操作系统并安装了下面这些软件的计算机(请参见本教程的参考资料部分以获取相关链接)： Groff。Groff分发版中包括groff前端工具、troff后端排版引擎和本教 程中使用的各种附属工具。 自由软件基金会将Groff作为其GNU Project中的一部分进行了发布，所 发布的源代码符合GNU通用公共许可证(GPL)并得到了广泛的移植，几乎对于所有的UNIX操作系统、以及非UNIX操作系统(如Microsoft?Windows?)都有相应 的可用版本。 在撰写本教程时，最新的Groff发布版是Version 1.19.2，对于学习本教 程而言，您至少需要Groff Version 1.17。 gxditview。从Version 1.19.2开始，Groff中包含了这个工具，而在以 前的版本中，对其进行了单独的发布。 PostScript Previewer，如ghostview、gv或showpage。 如果您是从源代码安装Groff，那么请参考Groff源代码分发版中的自述 文件，其中列举了所需的任何额外的软件，而在编译和安装Groff时可能需要 使用这些软件。 介绍Groff 用户通常在字处理软件、桌面发布套件和文本布局应用程序等应用程序环 境中创建文档，而在这些环境中，最终将对文档进行打印或导出为另一种格式。整个文档准备过程，从创建到最后的输出，都发生在单个应用程序中。文档通 TeX 使用指南 常见问题（一） 1.\makeatletter 和\makeatother 的用法？ 答：如果需要借助于内部有\@字符的命令，如\@addtoreset，就需要借助于另两个命令 \makeatletter, \makeatother。 下面给出使用范例，用它可以实现公式编号与节号的关联。 \begin{verbatim} \documentclass{article} ... \makeatletter % '@' is now a normal "letter" for TeX \renewcommand\theequation{\thesection.\arabic{equation}} \@addtoreset{equation}{section} \makeatother % '@' is restored as a "non-letter" character for TeX \begin{document} ... \end{verbatim} 2.比较一下CCT与CJK的优缺点？ 答：根据王磊的经验，CJK 比CCT 的优越之处有以下几点： 1）字体定义采用LaTeX NFSS 标准，生成的DVI 文件不必像CCT 那样需要用patchdvi 处理后才能预览和打印。而且一般GB 编码的文件也不必进行预处理就可直接用latex 编译。2）可使用多种TrueType 字体和Type1 字体，生成的PDF 文件更清楚、漂亮。 3）能同时在文章中使用多种编码的文字，如中文简体、繁体、日文、韩文等。 当然，CCT 在一些细节上，如字体可用中文字号，字距、段首缩进等。毕竟CJK 是老外作的吗。 谈到MikTeX 和fpTeX, 应该说谈不上谁好谁坏，主要看个人的喜好了。MikTeX 比较小，不如fpTeX 里提供的TeX 工具，宏包全，但一般的情况也足够了。而且Yap 比windvi 要好用。fpTeX 是teTeX 的Windows 实现，可以说各种TeX 的有关软件基本上都包括在内。 3.中文套装中如何加入新的.cls文件？ 答：放在tex文件的同一目录下，或者miktex/localtexmf/tex/latex/下的某个子目录下，可以自己建一个。 4.怎样象第几章一样，将参考文献也加到目录？ 答：在参考文献部分加入 \addcontentsline{toc}{chapter}{参考文献} 论文的写作格式及规范 附件9： 科学技术论文的写作格式及规范 用非公知公用的缩写词、字符、代号，尽量不出现数学式和化学式。 2作者署名和工作单位标引和检索，根据国家有关标准、数据规范为了提高技师、高级技师论文的学术质量，实现论文写的科学化、程序化和规范化，以利于科技信息的传递和科技情报的作评定工作，特制定本技术论文的写作格式及规范。望各位学员在注重科学研究的同时，做好科技论文撰写规范化工作。 1 题名 题名应以简明、确切的词语反映文章中最重要的特定内容，要符合编制题录、索引和检索的有关原则，并有助于选定关键词。 中文题名一般不宜超过20 个字，必要时可加副题名。英文题名应与中文题名含义一致。 题名应避免使作者署名是文责自负和拥有著作权的标志。作者姓名署于题名下方，团体作者的执笔人也可标注于篇首页地脚或文末，简讯等短文的作者可标注于文末。 英文摘要中的中国人名和地名应采用《中国人名汉语拼音字母拼写法》的有关规定；人名姓前名后分写，姓、名的首字母大写，名字中间不加连字符；地名中的专名和通名分写，每分写部分的首字母大写。 作者应标明其工作单位全称、省及城市名、邮编( 如“齐齐哈尔电业局黑龙江省齐齐哈尔市(161000) ”)，同时，在篇首页地脚标注第一作者的作者简介，内容包括姓名，姓别，出生年月，学位，职称，研究成果及方向。 3摘要 论文都应有摘要（3000 字以下的文章可以略去）。摘要的：写作应符合GB6447-86的规定。摘要的内容包括研究的目的、方法、结果和结论。一般应写成报道性文摘，也可以写成指示性或报道-指示性文摘。摘要应具有独立性和自明性，应是一篇完整的短文。一般不分段，不用图表和非公知公用的符号或术语，不得引用图、表、公式和参考文献的序号。中文摘要的篇幅：报道性的300字左右，指示性的100 字左右，报道指示性的200字左右。英文摘要一般与中文摘要内容相对应。 4关键词 关键词是为了便于作文献索引和检索而选取的能反映论文主题概念的词或词组，一般每篇文章标注3?8个。关键词应尽量从《汉语主题词表》等词表中选用规范词——叙词。未被词表收录的新学科、新技术中的重要术语和地区、人物、文献、产品及重要数据名称，也可作为关键词标出。中、英文关键词应一一对应。 5引言 引言的内容可包括研究的目的、意义、主要方法、范围和背景等。 应开门见山，言简意赅，不要与摘要雷同或成为摘要的注释，避免公式推导和一般性的方法介绍。引言的序号可以不写，也可以写为“ 0”，不写序号时“引言”二字可以省略。 6论文的正文部分 论文的正文部分系指引言之后，结论之前的部分，是论文的核心， 应按GB7713--87 的规定格式编写。 6.1层次标题公文写作规范格式
关于会议纪要的规范格式和写作要求
titlesec宏包使用手册
毕业论文写作要求与格式规范
公文格式规范与常见公文写作
ctex 宏包说明 ctex
文档书写格式规范要求
政府公文写作格式规范
tabularx宏包中改变弹性列的宽度
2-1论文写作要求与格式规范(2009年修订)
公文写作毕业论文写作要求和格式规范
配合前面的ntheorem宏包产生各种定理结构
论文写作格式规范与要求(完整资料).doc
Groff 应用
TeX 使用指南(常见问题)
论文的写作格式及规范
相关主题
文本预览