diff options
| -rw-r--r-- | papers/cfrontend_new/.genfiles | 109 | ||||
| -rwxr-xr-x | papers/cfrontend_new/Makefile | 22 | ||||
| -rwxr-xr-x | papers/cfrontend_new/blazy.bib | 1033 | ||||
| -rwxr-xr-x | papers/cfrontend_new/dynsem1.etex | 80 | ||||
| -rwxr-xr-x | papers/cfrontend_new/dynsem2.etex | 89 | ||||
| -rw-r--r-- | papers/cfrontend_new/dynsem3.etex | 48 | ||||
| -rwxr-xr-x | papers/cfrontend_new/dynsem4.etex | 42 | ||||
| -rwxr-xr-x | papers/cfrontend_new/infrules.sty | 224 | ||||
| -rw-r--r-- | papers/cfrontend_new/klunamed.bst | 1181 | ||||
| -rwxr-xr-x | papers/cfrontend_new/kluwer.cls | 2873 | ||||
| -rw-r--r-- | papers/cfrontend_new/macros.tex | 146 | ||||
| -rwxr-xr-x | papers/cfrontend_new/mymacros.sty | 221 | ||||
| -rwxr-xr-x | papers/cfrontend_new/paper.tex | 382 | ||||
| -rwxr-xr-x | papers/cfrontend_new/syntax.etex | 52 | ||||
| -rwxr-xr-x | papers/cfrontend_new/syntax2.etex | 44 | ||||
| -rw-r--r-- | papers/cfrontend_new/trace.etex | 19 | ||||
| -rwxr-xr-x | papers/cfrontend_new/values.etex | 40 |
17 files changed, 6605 insertions, 0 deletions
diff --git a/papers/cfrontend_new/.genfiles b/papers/cfrontend_new/.genfiles new file mode 100644 index 0000000..e14d46f --- /dev/null +++ b/papers/cfrontend_new/.genfiles @@ -0,0 +1,109 @@ +dynsem1.tex +dynsem2.tex +trace.tex +trace.tex +syntax2.tex +trace.tex +dynsem1.tex +dynsem2.tex +values.tex +values.tex +values.tex +values.tex +values.tex +values.tex +values.tex +values.tex +syntax2.tex +dynsem1.tex +dynsem2.tex +dynsem2.tex +dynsem2.tex +dynsem1.tex +dynsem2.tex +dynsem1.tex +dynsem2.tex +dynsem1.tex +dynsem1.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem2.tex +dynsem4.tex +dynsem4.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +syntax.tex +syntax.tex +syntax2.tex +values.tex +values.tex +syntax2.tex +values.tex +syntax2.tex +syntax2.tex +syntax2.tex +syntax2.tex +syntax2.tex +dynsem1.tex +dynsem1.tex +dynsem1.tex +dynsem1.tex +dynsem1.tex +dynsem1.tex +dynsem2.tex +dynsem2.tex +syntax.tex +syntax.tex +syntax.tex +syntax.tex +syntax2.tex +dynsem1.tex +dynsem2.tex +dynsem3.tex +dynsem4.tex +syntax2.tex +dynsem1.tex +dynsem2.tex +dynsem1.tex +dynsem1.tex +dynsem2.tex +syntax2.tex +dynsem2.tex +dynsem3.tex +dynsem1.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem2.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +dynsem3.tex +trace.tex +dynsem4.tex +dynsem2.tex +dynsem2.tex +syntax.tex +syntax.tex +dynsem4.tex +dynsem4.tex +dynsem2.tex +dynsem2.tex +dynsem2.tex +dynsem2.tex +dynsem3.tex +dynsem3.tex diff --git a/papers/cfrontend_new/Makefile b/papers/cfrontend_new/Makefile new file mode 100755 index 0000000..75d06d0 --- /dev/null +++ b/papers/cfrontend_new/Makefile @@ -0,0 +1,22 @@ + +LATEX=latex +PDFLATEX=pdflatex +TEXQUOTE=./texquote3 + +$(basename paper.tex): paper.tex macros.tex syntax.tex syntax2.tex values.tex dynsem1.tex dynsem2.tex dynsem3.tex dynsem4.tex trace.tex + $(PDFLATEX) paper.tex + +clean:: + rm -f `cat .genfiles` + rm -f *.log *.dvi *.blg *~ #*# .genfiles + +.SUFFIXES: .tex .etex .ftex + +.etex.tex: + $(TEXQUOTE) < $< > $*.tex + @echo $*.tex >> .genfiles + +.ftex.tex: + $(TEXQUOTE) < $< > $*.tex + @echo $*.tex >> .genfiles + diff --git a/papers/cfrontend_new/blazy.bib b/papers/cfrontend_new/blazy.bib new file mode 100755 index 0000000..d51242c --- /dev/null +++ b/papers/cfrontend_new/blazy.bib @@ -0,0 +1,1033 @@ +@String{CSM = {Proc. of the Conf. on Soft. Maintenance (CSM)}} +@String{PLDI = {Proc. of the Programming Languages Design and Implementation Conf. (PLDI)}} +@String{POPL = {Proc. of Principles Of Progamming Languages symposium (POPL)}} +@String{LNCS = {Lecture Notes in Computer Science}} +@String{TOPLAS = {ACM Transactions on Programing Languages and Systems}} +@String{SV = {Springer-Verlag}} +@String{JUCS = "Journal of Universal Computer Science"} + +@Book{B:book, + AUTHOR = "J.R. Abrial", + TITLE = "The B-Book assigning programs to meanings", + PUBLISHER="Cambridge University Press", + YEAR = "1996"} + +@Book{compil:book, + AUTHOR = "A.V. Aho and R.Sethi and J.D.Ullman", + TITLE = "Compilers: Principles, Techniques and Tools", + PUBLISHER="Addison-Wesley", + YEAR = "1988"} + +@phdthesis{C:andersen, + AUTHOR = "L.O. Andersen", + TITLE = "Program analysis and specialization for the C programming language", + YEAR="1994", + SCHOOL="University of Copenhagen", NOTE="DIKU report 94/19"} + +@InProceedings{ppc:appel, + author = {A.W. Appel}, + title = {Foundational Proof-Carrying Code}, + booktitle = {16th Annual IEEE Symp. on Logic in Computer Science (LICS)}, + year = {2001}, + month = {June}, + address = {Washington, DC, United States}, + pages = {247} +} + +@INPROCEEDINGS{pepm:glueck, + AUTHOR="R. Baier and R. Gl{\"u}ck and R. Z{\"o}chling", + TITLE="Partial evaluation of numerical programs in {F}ortran", + PAGES="119-132", + BOOKTITLE = "Proc. of the Partial Evaluation and semantics based Program Manipulation Workshop", + ORGANIZATION="ACM SIGPLAN", + ADDRESS="Melbourne", YEAR="1994"} + +@ARTICLE{slicing:berg, + AUTHOR="J.A. Bergstra and T.B. Dinesh and J. Field and J. Heering", + TITLE="Toward a complete transformational toolkit for compilers", + PAGES="639-684", + JOURNAL = TOPLAS, + VOLUME="19", NUMBER="5", + MONTH = "September", YEAR="1997"} + +@Book{CoqArt, + author = "Y. Bertot and P. Castéran", + title = {Interactive Theorem Proving and Program Development +Coq'Art: The Calculus of Inductive Constructions}, + publisher = {Springer Verlag}, + year = {2004}, +} + +@TechReport{bertot:compilo, + author = {Y. Bertot}, + title = {A certified compiler for an imperative langage}, + institution = {INRIA}, + year = {1998}, + number = {RR-3488} +} + +@inproceedings{coq:bertot95, + author = "Y. Bertot and R. Fraer", + title = "Reasoning with Executable Specifications", + booktitle = "{TAPSOFT '95}: Theory and Practice of Software Development", + series = LNCS, volume = "915", + publisher = "Springer-Verlag", + editor = "P. D. Mosses and M. Nielsen and M. I. Schwartzbach", + pages = "531--45", + ADDRESS = "Aarhus", MONTH = "May", year = "1995"} + +@PhdThesis{these:sb, + author = {S.Blazy}, + title = {La spécialisation de programmes pour l'aide à la maintenance du logiciel}, + school = {CNAM}, + year = {1993}, + month = {December} +} + +@INPROCEEDINGS{washington:sb, + AUTHOR = "S. Blazy and P. Facon", + TITLE = "{SFAC}, a tool for program comprehension by specialization", + BOOKTITLE = "Proc. of the Third Workshop on Program Comprehension", + ORGANIZATION = "IEEE", + PAGES = "162-167", + ADDRESS = "Washington D.C.", MONTH = "November", YEAR = {1994} } + +@INPROCEEDINGS{tapsoft:sb, + AUTHOR = "S. Blazy and P. Facon", + TITLE = "Formal specification and prototyping of a program specializer", + BOOKTITLE = "{TAPSOFT '95}: Theory and Practice of Software Development", + PAGES = "666-680", + SERIES = LNCS, VOLUME = "915", + publisher = "Springer-Verlag", + editor = "P. D. Mosses and M. Nielsen and M. I. Schwartzbach", + ADDRESS = "Aarhus", MONTH = "May", YEAR = {1995} } + +@INPROCEEDINGS{pe1996:sb, + AUTHOR = "S. Blazy and P. Facon", + TITLE = "An automatic interprocedural analysis for the understanding of scientific application + Programs", + PAGES = "1-16", + crossref={pe1996:tout} } + +@ARTICLE{sope:sb, + AUTHOR = "S. Blazy and P. Facon", + TITLE = "Partial evaluation for program understanding", + crossref={sope:tout} } + +@INPROCEEDINGS{ase:sb, + AUTHOR = "S. Blazy and P. Facon", + TITLE = "Application of formal methods to the development of a software maintenance tool", + BOOKTITLE = "Proc. of the Automated Software Engineering Conference", + PAGES = "162-171", + ORGANIZATION = "IEEE", + MONTH = "November", YEAR = {1997} } + +@article{sekejal:sb, + AUTHOR = "S. Blazy", + TITLE = "Partial Evaluation for the understanding of {F}ortran programs", + journal = "Journal of Software Engineering and Knowledge Engineering", + VOLUME = "4", NUMBER = "4", + PAGES = "535-559", + YEAR = {1994} } + +@article{asejal:sb, + AUTHOR = "S. Blazy", + TITLE = "Specifying and Automatically Generating a Specialization Tool for {F}ortran 90", + journal = "Journal of Automated Software Engineering", + VOLUME = "7", NUMBER = "4", + PAGES = "345-376", + MONTH = "December", YEAR = {2000} } + +@techreport{cedric02:sb, + title = "Transformations certifiées de programmes impératifs", + author = "S. Blazy", + type = "Technical report", + institution = "CEDRIC", + number = "398", + month = "December", + year = "2002", +} + +@INPROCEEDINGS{icfem:sb, + AUTHOR = "S. Blazy and X. Leroy", + TITLE = "Formal verification of a memory model for + {C}-like imperative languages", + BOOKTITLE = "Proc. of Int. Conf. on Formal Engineering Methods {ICFEM}", + PAGES = {280--299}, + SERIES = LNCS, VOLUME = 3785 , + publisher = "Springer-Verlag", + ADDRESS = "Manchester, UK", + MONTH = "November", + YEAR = {2005} +} + +@inproceedings{blazy06:fm, + author = {Sandrine Blazy and Zaynah Dargaye and + Xavier Leroy}, + title = {Formal Verification of a {C} Compiler Front-End}, + booktitle = {Symp. on Formal Methods (FM'06)}, + SERIES = {Lecture Notes in Computer Science}, + VOLUME = 4805, + year = {2006}, + pages = {460-475}, + ee = {http://dx.doi.org/10.1007/11813040_31}} + + +@InProceedings{table:ob, + author = {O. Boite and C. Dubois}, + title = {Proving {T}ype {S}oundness of a {S}imply {T}yped {ML}-like {L}anguage with {R}eferences}, + year = 2001, + Booktitle = {Supplemental Proc. of TPHOL'01, Informatics + Research Report EDI-INF-RR-0046 of University of Edinburgh}, + Editor = {R. Boulton and P. Jackson}, + pages = {69--84} +} + +@INPROCEEDINGS{coq:dataflow, + AUTHOR = {D. Cachera and T. Jensen and D. Pichardie and V. Rusu}, + TITLE = {{Extracting a Data Flow Analyser in Constructive Logic}}, + BOOKTITLE = {Proc.\ of 13th European Symp. on Programming (ESOP'04)}, + YEAR = {2004}, + PAGES = {385--400}, + NUMBER = {2986}, + SERIES = LNCS, + PUBLISHER = SV} +} + +@INPROCEEDINGS{pldi:carini, + AUTHOR = "R. Carini and M. Hind", + TITLE = "Flow-sensitive interprocedural constant propagation", + BOOKTITLE = PLDI, + ORGANIZATION="ACM SIGPLAN", + PAGES = "23-31", + ADDRESS = "La Jolla", + MONTH = "June", YEAR = {1995} } + +@misc{cavalcanti-procedures, + author = "Ana Cavalcanti and Augusto Sampaio and Jim Woodcock", + title = "Procedures, Parameters, And Substitution In The Refinement Calculus", + url = "citeseer.nj.nec.com/cavalcanti97procedures.html" } + +@MANUAL{Centaur, + TITLE = "Centaur 1.2 documentation", + ORGANIZATION = "INRIA", + YEAR = "1994" } + +@Misc{Coq, + title = {The {C}oq proof assistant}, + note = "http://coq.inria.fr" +} + +@INPROCEEDINGS{pldi:chase, + AUTHOR = "D.R. Chase and F.K. Zadeck", + TITLE = "Analysis of pointers and structures", + BOOKTITLE = PLDI, + ORGANIZATION="ACM SIGPLAN", + PAGES = "296-31", + ADDRESS = "White Plains", + MONTH = "June", YEAR = {1990} } + +@PhdThesis{chrzaszcz04phd, + author = {J. Chrz{\k a}szcz}, + title = {Modules in Type Theory with Generative Definitions}, + school = {Warsaw Univerity and University of Paris-Sud}, + year = 2004, + month = {January} +} + +@article{pe:conselproof, + author = "C. Consel and S.-C. Khoo", + title = "On-Line Off-Line Partial Evaluation: Semantic Specifications and Correctness Proofs", + journal = "Journal of Functional Programming", + volume = "5", + number = "4", + pages = "461-500", + year = "1995" } + +@InProceedings{pe:tutorial, + author = {C.Consel and O.Danvy}, + title = {Tutorial notes on partial evaluation}, + booktitle = POPL, + pages = {493-501}, + year = {1993}, +} + +@InProceedings{coq:courtieu, + author = {P. Courtieu}, + title = {Normalized types}, + booktitle = {CSL}, + year = {2001}, +} + +@INPROCEEDINGS{preuve:despeyroux, + AUTHOR = "J. Despeyroux", + TITLE = "Proof of translation in natural semantics", + BOOKTITLE = "Proc. of the Symposium on Logic in Computer Science", + ADDRESS = "Cambridge, USA", + MONTH = "June", YEAR = {1986} } + +@mastersthesis{stage:pointeurs, + AUTHOR = "N. Dubois and P. Sayarath", + TITLE = "Aide {\`{a}} la {compr\'{e}hension} et {\`{a}} la maintenance: + pointeurs pour la {sp\'{e}cialisation} de programmes", + MONTH = "June", YEAR="1996", + SCHOOL="IIE-CNAM", NOTE="in French"} + +@INPROCEEDINGS{pldi:emami, + AUTHOR = "M. Emami and R. Ghiya and L.J. Hendren", + TITLE = "Context-sensitive interprocedural points-to analysis in the presence of function pointers", + BOOKTITLE = PLDI, + ORGANIZATION="ACM SIGPLAN", + PAGES = "242-256", + MONTH = "June", YEAR = {1994} } + +@techreport {cite110, + title = "Modelling program compilation in the refinement calculus", + author = "C. J. Fidge", + type = "Technical report", + institution = "Software Verification Research Centre", + address = "School of Information Technology, + The University of Queensland, Brisbane 4072. Australia", + number = "97-22", + month = may, + year = "1997", + keywords = "refinement, compilers.", + abstract = "This report shows how compilation of high-level language +programs to assembler code can be formally represented in the +refinement calculus. New operators are introduced to widen the +modelling language to encompass assembler code. A compilation +strategy is then embodied as a set of derived refinement rules.", + url = "http://svrc.it.uq.edu.au/Bibliography/svrc-tr.html?97-22" +} + +@INPROCEEDINGS{slicing:field, + AUTHOR = "J. Field and G. Ramalingam and F. Tip", + TITLE = "Parametric program slicing", + BOOKTITLE = POPL, + ADDRESS = "San Francisco, USA", + PAGES = "379-392", + YEAR = {1995} } + +@InProceedings{fsets, + author = {J.-C. Filli{\^a}tre and P. Letouzey}, + title = {Functors for Proofs and Programs}, + booktitle = {{European Symposium on Programing, (ESOP)}}, + volume = 2986, + publisher = {Springer-Verlag}, + series = LNCS, + year = {2004}, + address = {Barcelona, Spain}, + month = {April}, +} + +@INPROCEEDINGS{caduceus, + AUTHOR = {J.-C. Filli\^atre and C. March\'e}, + TITLE = {{Multi-Prover Verification of C Programs}}, + BOOKTITLE = {6th Int. Conf. on Formal Engineering Methods (ICFEM)}, + YEAR = 2004, + ADDRESS = {Seattle}, + MONTH = {November}, + PUBLISHER = SV, + SERIES = LNCS, + VOLUME = 3308, + PAGES = {15--29} +} + +@INCOLLECTION{frazer:reverse, + AUTHOR = "A. Frazer", + TITLE = "Reverse engineering", + BOOKTITLE = "Software reuse and reverse engineering in practice", + PUBLISHER = "P.A.V. Hall", + YEAR = "1992", + PAGES = "209-243" } + +@ARTICLE{slicing:gallagher, + AUTHOR = "K. Gallagher and J.R. Lyle", + TITLE = "Using program slicing in software mainetnance", + JOURNAL = {ACM Trans. Soft. Eng.}, + VOLUME = {17}, NUMBER = {8}, + PAGES = "751-761", + YEAR = {1991} } + +@Article{Glesner:2003, + author = "S. Glesner", + title = "{Using Program Checking to Ensure the Correctness of Compiler Implementations}", + journal = JUCS, + year = "2003", + volume = "9", + number = "3", + pages = "191--222", + month = {March}} + +@inproceedings{verifix, + author = {G. Goos and W. Zimmermann}, + title = {Verification of Compilers}, + booktitle = {Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel)}, + year = {1999}, + pages = {201--230}, + publisher = SV, + address = {London, UK} + } + +@article{fpcc:coq, + author = {N. Hamid and Z. Shao and V. Trifonov and S. Monnier and Z. Ni}, + title = {A Syntactic Approach to Foundational Proof-Carrying Code}, + journal= {Journal of Automated Reasoning}, + volume = 31, + number={3-4}, + year= {2003}, + month= {September}, + pages= "191-229" +} + +@ARTICLE{natsem:hannan, + AUTHOR="J. Hannan", + TITLE="Extended natural semantics", + PAGES="123-152", + JOURNAL = "Journal of functional programming", + VOLUME="3", NUMBER="2", + MONTH = "April", YEAR="1993"} + +@INPROCEEDINGS{pe:haraldsson, + AUTHOR = "A. Haraldsson", + TITLE = "A partial evaluator and its Use for compiling iterative statements in Lisp", + BOOKTITLE = POPL, + ADDRESS = "Tucson", + YEAR = {1978} } + +@INPROCEEDINGS{pldi:horwitz, + AUTHOR = "R. Hasti and S. Horwitz", + TITLE = "Using static single assignment form to improve flow-insensitive pointer analysis", + BOOKTITLE = PLDI, + ORGANIZATION="ACM SIGPLAN", + PAGES = "97-105", + ADDRESS = "Montreal", + MONTH = "June", YEAR = {1998} } + +@inproceedings{pe:hatcliff95, + author = "J. Hatcliff", + title = "Mechanically Verifying the Correctness of an Offline Partial Evaluator", + booktitle = "Proc. of the 7th Int. Symp. on Programming Languages: Implementations, Logics and Programs", + month = "September", + series = LNCS, volume = "982", + publisher = "Springer-Verlag", + address = "Utrecht, The Netherlands", + editor = "M. Hermenegildo and S.D. Swierstra", + pages = "279--298", + year = "1995"} + +@article{hatcliff97computational, + author = "John Hatcliff and Olivier Danvy", + title = "A Computational Formalization for Partial Evaluation", + journal = "Mathematical Structures in Computer Science", + volume = "7", + number = "5", + pages = "507-541", + year = "1997"} + + +@Article{hoare:verif, + author = {T. Hoare}, + title = {The Verifying Compiler: a Grand Challenge for Computing Research}, + journal = {Journal of the ACM}, + year = {2003}, + volume = {50}, + number = {1}, + pages = {63-69}, + month = {January}, +} + +@article{jifeng93specification, + author = "{H. Jifeng} and J. P. Bowen", + title = "Specification, Verification and Prototyping of an Optimized Compiler", + journal = "Formal Aspects of Computing", + volume = "6", + number = "6", + pages = "643-658", + year = "1993" } + +@Book{VDM:book, + AUTHOR = "C.B. Jones", + TITLE = "Systematic development using VDM", + PUBLISHER="Prentice-Hall", + YEAR = "1990"} + +@Book{pe:book, + AUTHOR = "N.D. Jones and C.K. Gomard and P. Sestoft", + TITLE = "Partial evaluation and automatic program generation", + PUBLISHER="Prentice-Hall", + YEAR = "1993"} + +@inproceedings{natsem:kahn, + AUTHOR = "G.Kahn", + booktitle = {{Proc. of the Symp. on Theoretical Aspects of Comp. Science}}, + pages = {237-257}, + publisher = "Springer-Verlag", + SERIES = LNCS, VOLUME = "247", + title = {{Natural Semantics}}, + year = {1987} +} + +@INPROCEEDINGS{pldi:landi, + AUTHOR = "W. Landi and B.G. Ryder", + TITLE = "A safe approximate algorithm for interprocedural pointer aliasing", + BOOKTITLE = PLDI, + PAGES = "235-248", + ORGANIZATION="ACM SIGPLAN", + MONTH = "June", YEAR = {1992} } + +@inproceedings{lawall:sound, + author = "J. Lawall and P. Thiemann", + title = "Sound Specialization in the Presence of Computational Effects", + booktitle = "Theoretical Aspects of Computer Software", + series = LNCS, volume = "1281", + publisher = "Springer-Verlag", + pages = "165--190", + month = "September", + address = {Sendai, Japan}, + year = "1997"} + +@inproceedings{paul:sefm, + author= {D. Leinenbach and W. Paul and E. Petrova}, + title= {Towards the Formal Verification of a {C}0 Compiler}, + booktitle= {Proc. Conf. on Software Engineering and Formal Methods (SEFM)}, + month={September}, + year= 2005, + address= {Koblenz, Germany} +} + +@INPROCEEDINGS{rhodium:popl, + AUTHOR = "S.Lerner and T. Millstein and E. Rice and C. Chambers", + TITLE = "Automated soundness proofs for dataflow analyses and transformations", + BOOKTITLE = POPL, + ADDRESS = "Long Beach, United States", + YEAR = {2005} } + +@InProceedings{xl:jfla, + author = {X. Leroy}, + title = {Certification d'un Compilateur: Enjeux, Problèmes et Approches}, + booktitle = {Journées Francophones des Langages Applicatifs (JFLA)}, + year = {2004}, + month = {January}, + organization = {INRIA}, + note = {invited talk} +} + +@InProceedings{xl:popl, + author = {X. Leroy}, + title = {Formal certification of a compiler back-end, or: programming a compiler + with a proof assistant}, + booktitle = POPL, + year = {2006}, + month = "January", + address = {Charleston, USA}, + pages = "42--54", + publisher = "ACM Press" +} + +@TechReport{xl:cminor, + author = {X. Leroy}, + title = {Le langage Intermédiaire {C} minor}, + institution = {Concert technical report}, + year = {2003}, + month = {February}, +} + +@misc{xl:compcert-backend, + author = {X. Leroy}, + title = {The {Compcert} certified compiler back-end -- + commented {Coq} development}, + howpublished = {Available on-line at \citeurl{http://cristal.inria.fr/~xleroy/compcert-backend/}}, + year = {2006} +} + +@INPROCEEDINGS{fse:liang, + AUTHOR = "D. Liang and M.J. Harrold", + TITLE = "Efficient points-to analysis for whole-program analysis", + BOOKTITLE = "Proc. of ESEC/FSE joint Conf.", + ADDRESS = "Toulouse, France", + PAGES = "199-215", + SERIES = LNCS, VOLUME = "1687", + ORGANIZATION="ACM SIGSOFT", + MONTH = "September", YEAR = {1999} } + +@phdthesis{letouzey04, + author = "P. Letouzey", + month = "July", + school = "Universit{\'e} Paris-Sud", + title = "Programmation fonctionnelle certifi{\'e}e -- L'extraction de programmes dans l'assistant {Coq}", + year = "2004" +} + +@InProceedings{nipkow:pt, + author = {F. Mehta and T. Nipkow}, + title = {Proving pointer programs in higher-order logic}, + booktitle="Automated Deduction --- CADE-19", + editor="F. Baader", + year=2003, + publisher=SV, + series=LNCS, + volume={2741}, + pages={121--135}} + +} + +@InProceedings{seplog:ref, + author = {I. Mijajlovic and N. Torp-Smith}, + title = {Refinement in Separation Context}, + booktitle = {Second workshop on semantics, program anlysis and computing analysis for memory management (SPACE)}, + year = {2004}, + address = {Venice, Italy}, + month = {January}, +} + +@InProceedings{space:region, + author = {S.Monnier}, + title = {Typed regions}, + booktitle = {Second workshop on semantics, program anlysis and computing analysis for memory management (SPACE)}, + year = {2004}, + address = {Venice, Italy}, + month = {January}, +} + +@Book{muchnik:book, + AUTHOR = "S.S. Muchnick", + TITLE = "Advanced compiler-design and implementation", + PUBLISHER="Morgan Kaufmann", + YEAR = "1997"} + + + +@InProceedings{pcc:necula, + author = {G. Necula}, + title = {Proof Carrying Code}, + booktitle = POPL, + year = {1997}, + month = {January}, +} + +@InProceedings{tv:necula, + author = "G. Necula", + title = "Translation Validation for an Optimizing Compiler", + booktitle = "{ACM} {SIG\-PLAN} Conf. on Programming Language + Design and Implementation (PLDI)", + pages = "83--95", + year = "2000" +} + +@inproceedings{russes:C, + author = {V.A. Nepomniaschy and I.S. Anureev and A.V. Promsky}, + title = {Verification-Oriented Language {C}-Light and Its Structural + Operational Semantics.}, + booktitle = {Ershov Memorial Conference}, + year = {2003}, + pages = {103-111}, +} + +@inproceedings{tv:pnueli, + author = {A. Pnueli and M. Siegel and E. Singerman}, + title = {Translation Validation}, + booktitle = {Proc. of the 4th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS)}, + year = {1998}, + pages = {151--166}, + publisher = SV, + address = {London, UK} + } + +@inproceedings{cocv:pnueli, + author = {Y. Hu and C. Barrett and B. Goldberg and A. Pnueli}, + title = {Validating More Loop Optimizations}, + booktitle = {Workshop on Compiler Optimization Meets Compiler Verification (COCV)}, + year = {2005}, + address = {Edinburgh, UK} + } + + +@Book{nielson:book, + AUTHOR = "H.R. Nielson and F. Nielson", + TITLE = "Semantics with application - A formal introduction", + PUBLISHER="John Wiley and Sons", + YEAR = "1992"} + +@Book{intabs:book, + AUTHOR = "F. Nielson and H.R. Nielson and C. Hankin", + TITLE = "Principles of Program Analysis", + PUBLISHER="Springer-Verlag", + YEAR = "1999"} + +@INPROCEEDINGS{ase:consel, + AUTHOR = "R. Marlet and S. Thibault and C. Consel", + TITLE = "Mapping software architectures to efficient implementation via partial evaluation", + BOOKTITLE = "Proc. of the Automated Software Engineering Conference", + PAGES = "183-192", + ORGANIZATION = "IEEE", + MONTH = "November", YEAR = {1997} } + +@InProceedings{cil, + author = {G. Necula and S. McPeak and S.P. Rahul and W. Weimer}, + title = {CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs}, + booktitle = {Conf. on Compiler Construction (CC'02)}, + address = {Grenoble, France}, + year = {2002}, + month = {March}, +} + +@article{borger:C, + author = "{E. B{\"o}rger} and N.G. Fruja and V.Gervasi and R.F. St{\"a}rk", + title = "A high-level modular definition of the semantics of {C\#}", + journal = "Theoretical Computer Science", + volume = "336", + number = "2-3", + pages = "235-284", + year = "2005" } + +@InProceedings{gurevich:C, + author = "Y. Gurevich and J.K. Huggins", + title = "The Semantics of the {C} Programming Language", + booktitle = "Proc. of CSL'92 (Computer Science Logic)", + publisher = "Springer Verlag", + SERIES = LNCS, VOLUME = "702", + year = 1993, + pages = "274-308", +} + +@techreport{KleinN-Toplas, + author = {Gerwin Klein and Tobias Nipkow}, + title = {A Machine-Checked Model for a {Java}-Like Language, Virtual Machine and Compiler}, + number = {0400001T.1}, + institution= {National ICT Australia}, + month=mar, + year=2004, + note = "To appear in ACM TOPLAS"} +} + +@PhdThesis{Norrish:phd, + author = "M. Norrish", + title = "{C} formalised in HOL", + school = "University of Cambridge", + year = 1998, + month = "December" +} + + +@misc{norvell94machine, + author = "T. Norvell", + title = "Machine code programs are predicates too", + text = "Theodore S. Norvell. Machine code programs are predicates too. In David + Till, editor, Sixth Refinement Workshop, Workshops in Computing, pages 188--204. + Springer Verlag, 1994.", + year = "1994"} + +@article{palsberg93correctness, + author = "J. Palsberg", + title = "Correctness of Binding-Time Analysis", + journal = "Journal of Functional Programming", + volume = "3", + number = "3", + pages = "347-363", + year = "1993"} + +@PhdThesis{papaspyrou-1998-fscpl, + author = "N.S. Papaspyrou", + title = "A formal semantics for the {C} programming language", + school = "National Technical University of Athens", + year = 1998, + month = "February" +} + +@TechReport{strecker05:_compil_verif_c0, + author = {Martin Strecker}, + title = {Compiler Verification for {C0}}, + institution = {Universit{\'e} Paul Sabatier}, + year = 2005, + address = {Toulouse}, + month = {April} +} + +@inproceedings{rival:popl, + author = {X. Rival}, + title = {Symbolic transfer function-based approaches to certified compilation}, + booktitle = POPL, + year = {2004}, + pages = {1--13}, + location = {Venice, Italy}, + publisher = {ACM Press}, + } + +@manual{f90, + author = "S. Ramsden and F. Lin and M.A. Pettipher and G.S. Noland and J.M. Brooke", + title="{Fortran} 90: a conversion course for {F}ortran 77 programmers", + organization="Manchester and north {HC} {T\&EC}", + edition="Third", + year="1995" +} + +@Misc{coq:renard, + author = {C. Renard}, + title = {Un peu d'extensionnalité en {C}oq}, + note = {Université Paris VI}, + year = {2001}, + howpublished = {Mémoire de DEA}, + month = {September} +} + +@INPROCEEDINGS{rinard:compil, + AUTHOR ="M. Rinard and D. Marinov", + TITLE = "Credible compilation with pointers", + BOOKTITLE = "Workshop on Run-Time Result Verification (RTRV)", + address = {Trento, Italy}, + MONTH = "July", + YEAR = {1999} } + +@manual{f90:norme, + title="Programming language {Fortran 90}", + organization="ANSI", + address="New York", + year="1992", + note="ANSI X3.198-1992 and ISO/IEC 1539-1991(E)" +} + +@INPROCEEDINGS{ptr:sagiv, + AUTHOR = "M. Sagiv and T. Reps and R. Wilhelm", + TITLE = "Solving shape-analysis problems in languages with destructive updating", + BOOKTITLE = POPL, + MONTH = "January", YEAR = {1997} } + + + +@Book{sampaio:compil, + author = {A.Sampaio}, + title = {An algebraic approach to compiler design}, + publisher = {World Scientific}, + year = {1997}, + volume = {4}, + OPTnumber = {}, + series = {AMAST series in computing}, + OPTaddress = {}, + OPTedition = {}, + OPTmonth = {}, + OPTnote = {}, + OPTannote = {} +} + +@inproceedings{mem:crf, + author = {X. Shen and Arvind and L. Rudolph}, + title = {Commit-reconcile \& fences ({CRF}): a new memory model for architects and compiler writers}, + booktitle = {ISCA '99: Proc. of the 26th symposium on Computer architecture}, + year = {1999}, + pages = {150--161}, + location = {Atlanta, Georgia, United States}, + address = {Washington, DC, United States}, + } + +@INPROCEEDINGS{ptr:steens, + AUTHOR = "B. Steensgaard", + TITLE = "Points-to analysis in almost linear time", + BOOKTITLE = POPL, + PAGES = "32-41", + YEAR = {1996} } + +@inproceedings{coq:terrasse, + author = "D. Terrasse", + title = "Encoding Natural Semantics in {Coq}", + booktitle = "Proc. of the 4th Conf. on Algebraic Methodology and Software Technology", + publisher = SV, + SERIES = LNCS, VOLUME = "936", + address = "Montreal, Canada", + editor = "V. S. Alagar", + pages = "230--244", + year = "1995" } + +@mastersthesis{stage:vassallo, + AUTHOR = "R. Vassallo", + TITLE = "Ergonomie et {\'{e}volution} d'un outil de {compr\'{e}hension} de programmes", + MONTH = "June", YEAR="1996", + SCHOOL="IIE-CNAM", NOTE="in French"} + +@Article{Wand93, + author = "M. Wand", + title = "Specifying the Correctness of Binding-Time Analysis", + journal = "Journal of Functional Programming", + year = "1993", + volume = "3", + number = "3", + pages = "365--387", + month = "July"} + +@INPROCEEDINGS{pldi:wilson, + AUTHOR = "R.P. Wilson and M.S. Lam", + TITLE = "Efficient context-sensitive pointer analysis for C programs", + BOOKTITLE = PLDI, + PAGES = "1-12", + ORGANIZATION="ACM SIGPLAN", + MONTH = "June", YEAR = {1995} } + +@Book{formal:winskel, + AUTHOR = "G. Winskel", + TITLE = "The formal semantics of programming languages - an introduction", + PUBLISHER="MIT Press", + YEAR = "1993"} + +@INPROCEEDINGS{alias:ryder, + AUTHOR = "S. Zhang and B. Ryder and W. Landi", + TITLE = "Program decomposition for pointer aliasing: a step toward practical analyses", + BOOKTITLE = "Proc. of the Symp. on Foundations of Soft. Eng.", + ADDRESS = "San Francisco", + MONTH = "October", YEAR = "1996", + PAGES = "81-92" } + +@PROCEEDINGS{pe1996:tout, + editor = "O. Danvy and R. Gl{\"u}ck and P. Thiemann", + TITLE = "International seminar on partial evaluation", + ADDRESS = "Dagstuhl castle", + SERIES = LNCS, VOLUME = "1110", + publisher = SV, + MONTH = "February", YEAR = {1996} } + +@proceedings{sope:tout, + TITLE = "Symposium on partial evaluation", + SERIES = "ACM Computing Surveys", + ORGANIZATION = "ACM", + NUMBER = "4", + MONTH = "December", YEAR = {1998} } + +@TechReport{outil:2, + author = {M.G.J. van den Brand and P. Klint and C. Verhoef}, + title = {{R}everse engineering and system renovation: an annotated bibliography}, + institution = {{U}niversity of {A}msterdam, {P}rogramming {R}esearch {G}roup}, + number = {P9603}, + year = {1996}, + fileurl = {http://ftp.wins.uva.nl/pub/programming-research/reports/1996/P9603.ps.Z}, + abstracturl = {http://ftp.wins.uva.nl/pub/programming-research/reports/1996/abstracts/P9603.txt}, +} + +@TechReport{P9702, + author = {M.G.J. van den Brand and M.P.A. Sellink and C. Verhoef}, + title = {{R}eengineering {COBOL} {S}oftware {I}mplies {S}pecification of the + {U}nderlying {D}ialects}, + institution = {{U}niversity of {A}msterdam, {P}rogramming {R}esearch {G}roup}, + number = {P9702}, + year = {1997}, + fileurl = {http://ftp.wins.uva.nl/pub/programming-research/reports/1997/P9702.ps.Z}, + abstracturl = {http://ftp.wins.uva.nl/pub/programming-research/reports/1997/abstracts/P9702.txt}, + note = {Available by anonymous ftp from ftp.wins.uva.nl, + file pub/programming-research/reports/1997/P9702.ps.Z} +} + +@INPROCEEDINGS{outil:3, + author = {M.P.A. Sellink and C. Verhoef}, + title = {Scaffolding for Software Renovation}, + BOOKTITLE = CSM, + ORGANIZATION = "IEEE", + ADDRESS = "Z{\"u}rich", MONTH = "March", YEAR = "2000", +} + +@INPROCEEDINGS{outil:4, + author = {H. Yank and P. Luker and W.Chu}, + title = {Code understanding through program transformation for reusable component identification}, + BOOKTITLE = "Fifth Workshop on Program Comprehension Proceedings", + ORGANIZATION = "IEEE", + YEAR = "1997", +} + +@INPROCEEDINGS{outil:1, + author = {I. Baxter and A. Yahin and L. Moura and M. Sant'Anna and L. Bier}, + title = {Clone detection using abstract syntax trees}, + BOOKTITLE = CSM, + ORGANIZATION = "IEEE", + YEAR = "1998", +} + +@article{mem:sota, + AUTHOR = "R.D. Tennent and D.R. Ghica and ", + TITLE = "Abstract models of storage", + journal = "Higher-Order and Symbolic Computation", + volume = "13", + number = "1/2", + MONTH = "", YEAR = "2000", + PAGES = "119-129" } + + + +@INPROCEEDINGS{mem:bornat, + AUTHOR = "R. Bornat", + TITLE = "Proving pointer programs in {H}oare logic", + BOOKTITLE = "5th Conf. on Mathematics of Program Construction", + publisher = SV, + MONTH = "", YEAR = "2000", + PAGES = "102-126" } + +@PROCEEDINGS{space:tout, + TITLE = "Second workshop on semantics, program analysis, and computing environments for memory management", + ADDRESS = "Venice", + ORGANIZATION="ACM SIGPLAN", + MONTH = "January", YEAR = {2004} } + +@InProceedings{typebin:popl, + author = {Z. Shao and B.Saha and V. Trifonov and N. Papaspyrou}, + title = {A type system for certified binaries}, + booktitle = POPL, + year = {2002}, + address = {Portland, United States}, + month = {January}, + pages = "217-232" +} + +@InProceedings{shao:cac, + author = {D.Yu and Z. Shao}, + title = {Verification of safety properties for concurrent assembly code}, + booktitle = {Int. Conf. on Functional Programming (ICFP)}, + year = {2004}, + address = {Snowbird, United States}, + month = {September}, + pages = "175-188" +} + + @InProceedings{walker:space, + author = {D. Walker}, + title = {Stacks, heaps and regions: one logic to bind them}, + year = {2004}, +booktitle = {Second workshop on semantics, program anlysis and computing analysis for memory management (SPACE)}, + note = {invited talk}, + address = {Venice, Italy}, + month = {January}, +} + + + +@InProceedings{mem:watson, + author = {G.Watson}, + title = {Compilation of refinement for a practical language}, + booktitle = {Proc. of the 5th Int. Conf. on Formal Engineering Methods (ICFEM)}, + crossref = {icfem2003} +} + +@Misc{concert, + title = {ARC Concert}, + note = {http://www-sop.inria.fr/lemme/concert}, +} + + +@proceedings{icfem2003, + editor = {J. S. Dong and J. Woodcock}, + title = {Proc. of the 5th Int. Conf. on Formal Engineering Methods, ICFEM 2003}, + publisher = SV, + series = LNCS, + volume = {2885}, + address = {Singapore}, + year = {2003}, + month = {November} +} + +@article{dave:survey, + author = {Maulik A. Dave}, + title = {Compiler verification: a bibliography}, + journal = {SIGSOFT Softw. Eng. Notes}, + volume = {28}, + number = {6}, + year = {2003}, + pages = {2--2}, + urlpublisher = {http://doi.acm.org/10.1145/966221.966235}, + publisher = "ACM Press" +} + diff --git a/papers/cfrontend_new/dynsem1.etex b/papers/cfrontend_new/dynsem1.etex new file mode 100755 index 0000000..136c0cd --- /dev/null +++ b/papers/cfrontend_new/dynsem1.etex @@ -0,0 +1,80 @@ +\begin{figure} + +\numberrules + +Expressions in l-value position: +\begin{pannel} + +\irule + E(\id) = b + -------------------------------------------------- + G, E |- \id^\tau, M \evallvalue (b, 0), \E0, M +\end \label{rule:1} + +\irule +% G, E |- a, M \evalexpr {\tt Vptr}(\loc), \tr, M' + G, E |- a, M \evalexpr \loc, \tr, M' + -------------------------------------------------- + G, E |- (\hbox{"*"}a)^\tau, M \evallvalue \loc, \tr, M' +\end \label{rule:2} + +\irule + G, E |- \unannot{a_1}{\tau_1}, M \evalexpr v_1, \tr_1, M_1 \\ + G, E |- \unannot{a_2}{\tau_2}, M_1 \evalexpr v_2, \tr_2, M_2 \\ + "add" (v_1, \tau_1, v_2, \tau_2) = \some{\loc} + -------------------------------------------------- + G, E |- (\unannot{a_1}{\tau_1} [\unannot{a_2}{\tau_2}])^\tau, M \evallvalue \loc, \cat {\tr_1} \tr_2, M_2 +\end \label{rule:3} + +\irule + G, E |- \unannot{a}{\tau}, M \evallvalue (b,\ofs), \tr, M' \\ + \tau = "Tstruct" (\id, \fl) & +% "type_of" (a) = "Tstruct" (\id, \fl) & + "field_offset" (f, \fl) = \some{\delta} + -------------------------------------------------- + G, E |- (\unannot{a}{\tau} \dot f)^{\tau_s}, M \evallvalue (b,\ofs + "repr" (\delta)), \tr, M' +\end \label{rule:4} + +\irule + G, E |- \unannot{a}{\tau}, M \evallvalue \loc, \tr, M' & + \tau = "Tunion" (\id, \fl) + -------------------------------------------------- + G, E |- (\unannot{a}{\tau} \dot f)^{\tau_u}, M \evallvalue \loc, \tr, M' +\end \label{rule:5} + +\end{pannel} +Expressions in r-value position: +\begin{pannel} + +\irule + G, E |- \unannot{a}\tau, M \evallvalue \loc, \tr, M' & + "loadval" (\tau, M', \loc) = \some{v} + -------------------------------------------------- + G, E |- \unannot{a}\tau, M \evalexpr v, \tr, M' +\end \label{rule:6} + +\irule + G, E |- a, M \evallvalue \loc, \tr, M' + -------------------------------------------------- + G, E |- (\hbox{"&"}a)^\tau, M \evalexpr \loc, \tr, M' +\end \label{rule:7} + +\irule + G, E |- \unannot{a_1}{\tau_1}, M \evalexpr v_1, \tr_1, M_1 & + G, E |- \unannot{a_2}{\tau_2}, M_1 \evalexpr v_2, \tr_2, M_2 \\ + "eval_binary_operation" (\op, v_1,\tau_1, v_2,\tau_2) = \some{v} + -------------------------------------------------- + G, E |- (\unannot{a_1}{\tau_1} \op \, \unannot{a_2}{\tau_2})^\tau, M \evalexpr v, \cat \tr_1 \tr_2, M_2 +\end \label{rule:8} + +\irule + G, E |- \unannot{a}{\tau_a}, M \evalexpr v', \tr, M' & + "cast" (v',\tau_a,\tau) = \some{v} + -------------------------------------------------- + G, E |- ((\tau)\unannot{a}{\tau_a}))^\tau, M \evalexpr v, \tr, M' +\end \label{rule:9} +\end{pannel} + +\caption{Selected rules of the dynamic semantics of Clight (expression evaluation)} +\label{fig:dynsem1} +\end{figure} diff --git a/papers/cfrontend_new/dynsem2.etex b/papers/cfrontend_new/dynsem2.etex new file mode 100755 index 0000000..e6f8163 --- /dev/null +++ b/papers/cfrontend_new/dynsem2.etex @@ -0,0 +1,89 @@ +\begin{figure} + +\numberrules + +Statements: +\begin{pannel} + +\srule G, E |- "skip", M \evalstmt "Out_normal", \E0, M +\end +\label{rule:10} + +\\[2mm] +\srule G, E |- "break", M \evalstmt "Out_break", \E0, M +\end +\label{rule:13} + +\\[2mm] +\srule G, E |- "continue", M \evalstmt "Out_continue", \E0, M +\end +\label{rule:14} + +\irule + G, E |- a, M \evalexpr v, \tr, M' + -------------------------------------------------- + G, E |- a , M \evalstmt \out, \tr, M' +\end \label{rule:11} + +\irule + G, E |- \unannot{a_1}{\tau}, M \evallvalue \loc, \tr_1, M_1 & + G, E |- \unannot{a_2}{\tau'}, M_1 \evalexpr v, \tr_2, M_2 \\ + "storeval"(\tau,M_2,\loc,v) = \some{M_3} + -------------------------------------------------- + G, E |- {(\unannot{a_1}{\tau} \hbox{" = "} \unannot{a_2}{\tau'})}^{\tau}, M \evalexpr v, \cat {\tr_1} \tr_2, M_3 +\end \label{rule:12} + +\\ +\irule + G, E |- s_1, M \evalstmt "Out_normal", \tr_1, M_1 & + G, E |- s_2, M_1 \evalstmt \out, \tr_2, M_2 + -------------------------------------------------- + G, E |- (s_1 ; s_2), M \evalstmt \out, \cat {\tr_1} \tr_2, M_2 +\end \label{rule:15} + +\irule + G, E |- s_1, M \evalstmt out, \tr, M' & + out \not= "Out_normal" + -------------------------------------------------- + G, E |- (s_1; s_2), M \evalstmt \out, \tr, M' +\end \label{rule:16} + +\\ +\irule + G, E |- a, M \evalexpr v, \tr, M' & "is_false"(v) + -------------------------------------------------- + G, E |- ("while" (a) ~ s), M \evalstmt "Out_normal", \tr, M' +\end \label{rule:17} + +\irule + G, E |- a, M \evalexpr v, \tr_1, M_1 & "is_true" (v) \\ + G, E |- s, M_1 \evalstmt \out, \tr_2, M_2 \\ + \out \in \{"Out_break", "Out_return", "Out_return" (v)\} + -------------------------------------------------- + G, E |- ("while" (a)~s), M \evalstmt "Out_normal", \cat {\tr_1} \tr_2, M_2 +\end \label{rule:18} + +\irule + G, E |- a, M \evalexpr v_a, \tr_1, M_1 & "is_true" (v_a) \\ + G, E |- s, M_1 \evalstmt ("Out_normal" \mid "Out_continue"), \tr_2, M_2 \\ + G, E |- ("while" (a)~s), M_2 \evalstmt \out', \tr_3, M_3 + -------------------------------------------------- + G, E |- ("while" (a)~s), M \evalstmt \out', \cat {\cat {\tr_1} \tr_2} \tr_3, M_3 +\end \label{rule:19} + +\\ +\srule + G, E |- ("return" \, \None), M \evalstmt "Out_return" , \tr, M +\end \label{rule:20} + +\\ +\irule + G, E |- a, M \evalexpr v, \tr, M' + -------------------------------------------------- + G, E |- ("return" \some a), M \evalstmt "Out_return" (v), \tr, M' +\end \label{rule:21} + +\end{pannel} +\caption{Selected rules of the dynamic semantics of Clight (statements execution)} +\label{fig:dynsem2} +\end{figure} diff --git a/papers/cfrontend_new/dynsem3.etex b/papers/cfrontend_new/dynsem3.etex new file mode 100644 index 0000000..bddcef6 --- /dev/null +++ b/papers/cfrontend_new/dynsem3.etex @@ -0,0 +1,48 @@ +\begin{figure} +Compatibility between values, outcomes and return types: + +$$\begin{array}{rclr} +"Out_normal", "Tvoid" & \# & "Vundef"& \\ +"Out_normal", "Tvoid" & \# & "Vundef"& \\ +"Out_return", \, "Tvoid" & \# & "Vundef" & \\ +"Out_return" \some v, \, \tau & \# & v & \mbox{when}\,\tau~\not="Tvoid" +\end{array}$$ + +\numberrules + +Function calls: +\begin{pannel} + +\irule + G, E |- {a_{fun}}^{\tau}, M \evalexpr v_{fun}, \tr_1, M_1 & + G, E |- a_{args}, M_1 \evalexpr v_{args}, \tr_2, M_2 \\ + G[v_{fun}] = \some{f} & + "type_of_fundef" (f) = \tau \\ + G |- f(v_{args}), M_2 \evalfunc v_{res}, \tr_3, M_3 + -------------------------------------------------- + G, E |- {({a_{fun}}^{\tau} (a_{args}))}^{\tau'}, M \evalexpr v_{res}, \cat {\cat {\tr_1} \tr_2} \tr_3, M_3 +\end \label{rule:25} +\end{pannel} + +Function invocations: +\begin{pannel} + +\irule + "alloc" ({\it \emptyset_E}, M, "params" (f) + "vars" (f),E) = (M_1, b) \\ + "bind_params" (E, M_1, "params" (f), v_{args}) = M_2 \\ + G, E |- "body" (f), M_2 \evalstmt \out, \tr, M_3 \\ + \out, \, "fn_return" (f) \, "#" \, v_{res} + -------------------------------------------------- + G, E |- f(v_{args}), M \evalstmt v_{res}, \tr, "free" (M_3, b) +\end \label{rule:26} + +\irule + v_{args}, v_{res} \cong^{\sigma} e_{args}, e_{res} + -------------------------------------------------- + G, E |- <\id \, \sigma>(v_{args}), M \evalstmt v_{res}, [\id \,e_{args}\, e_{res}], M +\end \label{rule:27} + +\end{pannel} +\caption{Dynamic semantics of function call} +\label{fig:dynsem3} +\end{figure} diff --git a/papers/cfrontend_new/dynsem4.etex b/papers/cfrontend_new/dynsem4.etex new file mode 100755 index 0000000..3f0b10a --- /dev/null +++ b/papers/cfrontend_new/dynsem4.etex @@ -0,0 +1,42 @@ +\begin{figure} + +\numberrules + +Execution of a "switch" statement: +\begin{pannel} + +\irule + G, E |- a, M \evalexpr n, \tr, M_1 \\ + G, E |- "select_switch" (n,\ls), M_1 \evalstmt \out, \tr_2, M_2 + -------------------------------------------------- + G, E |- "switch" (a)\ls, M \evalstmt "outcome_switch" (\out), \cat {\tr_1} \tr_2, M_2 +\end \label{rule:28} +\end{pannel} + +Execution of a "switch" branch: +\begin{pannel} + +\irule + G, E |- s, M \evalstmt \out, \tr, M' + -------------------------------------------------- + G, E |- "default" (s) , M \evalstmt \out, \tr, M' +\end \label{rule:29} + +\\ +\irule + G, E |- s, M \evalstmt "Out_normal", \tr_1, M_1 \\ + G, E |- \ls, M \evalstmt \out, \tr_2, M_2 + -------------------------------------------------- + G, E |- "case" (n,s,\ls), M \evalstmt \out', \tr_2, M_2 +\end \label{rule:30} +\\ +\irule + G, E |- s, M \evalstmt \out, \tr, M' & \out \not= "Out_normal" + -------------------------------------------------- + G, E |- "case" (n,s,\ls), M \evalstmt \out', \tr, M' +\end \label{rule:31} + +\end{pannel} +\caption{Dynamic semantics of switch statement} +\label{fig:dynsem4} +\end{figure} diff --git a/papers/cfrontend_new/infrules.sty b/papers/cfrontend_new/infrules.sty new file mode 100755 index 0000000..030fe51 --- /dev/null +++ b/papers/cfrontend_new/infrules.sty @@ -0,0 +1,224 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Style to compose inference rules + +% User commands: +% For axioms: +% \srule blah blah blah \end +% For inference rules: +% \irule premise1 & premise2 \\ +% premise3 & premise 4 +% --------------- +% conclusion +% \end +% Premises are separated by & (horizontal concatenation) +% or \\ (newline). The row of dashes must contain at least 4 dashes. +% To build derivations: use +% {\subrule premises ----- conclusion \end} +% for sub-derivations + +% Turnstyle: |- is recognized and becomes the turnstyle symbol. Works also +% outside of inference rules. |blabla- is a turnstyle symbol with "blabla" +% under the horizontal bar. + +% Layout of the rules: +% - by default: one rule per line, centered (display math mode) +% - inside \begin{pannel}...\end{pannel}: +% puts several rules per line, if possible. +% The rules are centered and evenly spread on the page. +% The rules are separated by at least 2em of space. +% - inside \begin{centerpannel}...\end{centerpannel}: +% same as {pannel}, but the rules are grouped in the middle +% of the line (with 1em space between them), instead of +% being spread out evenly. +% - inside \begin{simplepannel}...\end{simplepannel}: +% same as {pannel}, but no space is inserted between the rules. +% The user is expected to put the correct amount of space by +% hand. +% In all three "pannel" environments, \\ forces a newline. + +% Numbering rules: +% By default: no numbers. +% Use \numberrules to turn numbering on, \nonumberrules to turn it off. +% Also, use \nsrule axiom \end and \nirule premises ---- conclusion \end +% to number a single rule. +% Use \label{...} just after \end to label the rule number. +% Do \rulenumber=10 to restart numbering at rule number 10. +% Use \irulenumber{10} premises ---- conclusion \end +% and \srulenumber{10} axiom \end +% to number the rule with a given number (10, in this example). + +% User-definable dimensions: +% \ampersandskip amount of horizontal space inserted at & (default: 1.5em) + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% Turnstyle + +\let\|=| +\catcode`|=\active +\def|{\@ifnextchar-{\simpleturnstile}{\annotturnstile}} +\def\simpleturnstile-{\vdash} +\def\annotturnstile#1-{% + \vdash_{\!\!\!\lower0.05ex\hbox{\tiny #1}}} + +% Here is a list of the characters that have been specially catcoded: +\def\dospecials{\do\ \do\\\do\{\do\}\do\$\do\&% + \do\#\do\^\do\_\do\%\do\~\do\|} +\def\docspecials{\do\ \do\$\do\&% + \do\#\do\^\do\^^K\do\_\do\^^A\do\%\do\~\do\|} + +% Definition of & + +\def\ampersandskip{1.5em} +\def\amper{\hspace*{\ampersandskip}\relax} +{\catcode`&=\active \global\def&{\amper}} + +% Inference rules + +\def\mathmode{$$} %overriden by the pannel environments +\def\endmathmode{$$} %ditto + +\def\irule{\mathmode\catcode`&=\active\begin{array}{@{}c@{}}\@irule} + +\def\@irule#1----#2\end{ + #1 + \\[-1.2ex] \hrulefill \hbox to 0pt{\@makerulenumber\hss} \\ \relax + \@gobbledashes #2 + \end{array}% + \@rulenumber% + \endmathmode} + +% Skip any dashes at the beginning of the argument + +\def\@gobbledashes#1{% + \ifx-#1\let\@next=\@gobbledashes\else\let\@next=#1\fi\@next% +} + +% Axioms + +\def\srule{\mathmode\catcode`&=\active\begin{array}{@{}c@{}}\@srule} + +\def\@srule#1\end{#1\end{array}\hbox to 0pt{\@makerulenumber\hss}\@rulenumber\endmathmode} + +% Sub-rules + +\def\subrule#1----#2\end{ + \begin{array}[b]{@{}c@{}} + #1 + \\[-1.2ex] \hrulefill \\ \relax + \@gobbledashes #2 + \end{array}} + +\def\subrulenum#1----#2\end{ + \begin{array}[b]{@{}c} + #1 + \\[-1.2ex] \hrulefill \hbox to 0pt{\@makerulenumber\hss} \\ \relax + \@gobbledashes #2 + \end{array} + \@rulenumber} + +% Rule numbering + +\def\rulenumberskip{0.5em} +\def\@rulenumber{} +\def\@makerulenumber{} + +\def\skiprulenumber{\setbox0=\hbox{\@makerulenumber}\hspace*{\wd0}} + +\newcount\rulenumber +\rulenumber=1 + +\def\numberrules{ + \def\@makerulenumber{% + \kern\rulenumberskip\rm(\the\rulenumber)}% + \def\@rulenumber{% + \skiprulenumber% + \global\edef\@currentlabel{\the\rulenumber}% + \global\advance\rulenumber by1}} + +\def\nonumberrules{ + \def\@rulenumber{}} + +% To number just one rule + +\def\@numberonerule{ + \def\@makerulenumber{% + \kern\rulenumberskip\rm(\the\rulenumber)}% + \def\@rulenumber{% + \skiprulenumber% + \global\edef\@currentlabel{\the\rulenumber}% + \global\advance\rulenumber by1% + \global\def\@makerulenumber{}% + \global\def\@rulenumber{}}} + +\def\nirule{\@numberonerule\irule} +\def\nsrule{\@numberonerule\srule} + +% To number just one rule with a given number + +\def\@setrulenumber#1{% + \def\@makerulenumber{% + \kern\rulenumberskip\rm(#1)}% + \def\@rulenumber{% + \skiprulenumber% + \global\def\@makerulenumber{}% + \global\def\@rulenumber{}}% +} + +\def\@tempsetrulenumber#1{% + \def\@makerulenumber{% + \kern\rulenumberskip\rm(#1)}% + \def\@rulenumber{% + \skiprulenumber}% + +} + +\def\irulenumber#1{\@setrulenumber{#1}\irule} +\def\srulenumber#1{\@setrulenumber{#1}\srule} + +\def\subrulenumber#1{\@tempsetrulenumber{#1}\subrulenum} + +% \begin{pannel} ... \end{pannel} puts several rules per line +% whenever possible. The rules are centered on the page and evenly spread. + +\def\pannel{% +\begin{center}% +\def\mathmode{\hfilneg\hfil\hskip 1em$\displaystyle}% +\def\endmathmode{$\hskip 1em\hfil}% +\lineskip=1.5ex plus 0.4ex minus 0.1ex% +\catcode`\^^M=10% space +} + +\def\endpannel{% + \end{center}% +} + +% Same as pannel, except that the rules are grouped in the middle of +% the page + +\def\centerpannel{ + \begin{center} + \def\mathmode{$\displaystyle} + \def\endmathmode{$\hskip 1em} + \lineskip=1.5ex plus 0.4ex minus 0.1ex + \catcode`\^^M=10 %space +} + +\def\endcenterpannel{ + \end{center} +} + +% Same as pannel, except that no space is inserted between rules. +% The user is resonsible for inserting the correct amount of space. + +\def\simplepannel{ + \begin{center} + \def\mathmode{$\displaystyle} + \def\endmathmode{$} + \lineskip=1.5ex plus 0.4ex minus 0.1ex + \catcode`\^^M=10 %space +} + +\def\endsimplepannel{ + \end{center} +} diff --git a/papers/cfrontend_new/klunamed.bst b/papers/cfrontend_new/klunamed.bst new file mode 100644 index 0000000..81e9bd5 --- /dev/null +++ b/papers/cfrontend_new/klunamed.bst @@ -0,0 +1,1181 @@ +% This style produces citations in the `author-year' format. +% It supports two forms of citation: the \cite command produces: (Author, year) +% in the text; the \cite* command only: (year) . + + +ENTRY + { address + author + booktitle + chapter + edition + editor + howpublished + institution + journal + key + note + number + organization + pages + publisher + school + series + title + type + volume + year + } + {} + { label extra.label sort.label } + +INTEGERS { output.state before.all mid.sentence after.sentence + after.block after.colon } + +FUNCTION {init.state.consts} +{ #0 'before.all := + #1 'mid.sentence := + #2 'after.sentence := + #3 'after.block := + #4 'after.colon := +} + +STRINGS { s t } + +FUNCTION {output.nonnull} +{ 's := + output.state mid.sentence = + { ", " * write$ } + { output.state after.block = + { add.period$ write$ + newline$ + "\newblock " write$ + } + { output.state before.all = + 'write$ + { output.state after.colon = + 'write$ + { add.period$ " " * write$ } + if$ + } + if$ + } + if$ + mid.sentence 'output.state := + } + if$ + s +} + +FUNCTION {output.nonnull.extra} +{ 's := + output.state mid.sentence = + { " " * write$ } + { output.state after.block = + { add.period$ write$ + newline$ + "\newblock " write$ + } + { output.state before.all = + 'write$ + { output.state after.colon = + 'write$ + { add.period$ " " * write$ } + if$ + } + if$ + } + if$ + mid.sentence 'output.state := + } + if$ + s +} + +FUNCTION {output} +{ duplicate$ empty$ + 'pop$ + 'output.nonnull + if$ +} + +FUNCTION {output.extra} +{ duplicate$ empty$ + 'pop$ + 'output.nonnull.extra + if$ +} + +FUNCTION {output.check} +{ 't := + duplicate$ empty$ + { pop$ "empty " t * " in " * cite$ * warning$ } + 'output.nonnull + if$ +} + +FUNCTION {output.check.extra} +{ 't := + duplicate$ empty$ + { pop$ "empty " t * " in " * cite$ * warning$ } + 'output.nonnull.extra + if$ +} + +FUNCTION {output.year.check} +{ year empty$ + { "empty year in " cite$ * warning$ } + { write$ + ": " year * extra.label * + mid.sentence 'output.state := + } + if$ +} + +FUNCTION {output.bibitem} +{ newline$ + "\bibitem[" write$ + label write$ + "]{" write$ + cite$ write$ + "}" write$ + newline$ + "" + before.all 'output.state := +} + +FUNCTION {fin.entry} +{ add.period$ + write$ + newline$ +} + +FUNCTION {new.block} +{ output.state before.all = + 'skip$ + { after.block 'output.state := } + if$ +} + +FUNCTION {new.sentence} +{ output.state after.block = + 'skip$ + { output.state before.all = + 'skip$ + { after.sentence 'output.state := } + if$ + } + if$ +} + +FUNCTION {not} +{ { #0 } + { #1 } + if$ +} + +FUNCTION {and} +{ 'skip$ + { pop$ #0 } + if$ +} + +FUNCTION {or} +{ { pop$ #1 } + 'skip$ + if$ +} + +FUNCTION {new.block.checkb} +{ empty$ + swap$ empty$ + and + 'skip$ + 'new.block + if$ +} + +FUNCTION {field.or.null} +{ duplicate$ empty$ + { pop$ "" } + 'skip$ + if$ +} + +FUNCTION {boldface} +{ duplicate$ empty$ + { pop$ "" } + { "{\bf " swap$ * "}" * } + if$ +} + +FUNCTION {emphasize} +{ duplicate$ empty$ + { pop$ "" } + { "{\em " swap$ * "}" * } + if$ +} + +INTEGERS { nameptr namesleft numnames } + +FUNCTION {format.names} +{ 's := + #1 'nameptr := + s num.names$ 'numnames := + numnames 'namesleft := + { namesleft #0 > } + { nameptr #1 > + { s nameptr "{f. }{vv~}{ll}{, jj}" format.name$ 't := } + { s nameptr "{vv~}{ll}{, jj}{, f.}" format.name$ 't := } + if$ + nameptr #1 > + { namesleft #1 > + { ", " * t * } + { numnames #2 > + { "," * } + 'skip$ + if$ + t "others" = + { " et~al." * } + { " and " * t * } + if$ + } + if$ + } + 't + if$ + nameptr #1 + 'nameptr := + namesleft #1 - 'namesleft := + } + while$ +} + +FUNCTION {format.ed.names} +{ 's := + #1 'nameptr := + s num.names$ 'numnames := + numnames 'namesleft := + { namesleft #0 > } + { nameptr #1 > + { s nameptr "{f. }{vv~}{ll}{, jj}" format.name$ 't := } + { s nameptr "{f. }{vv~}{ll}{, jj}" format.name$ 't := } + if$ + nameptr #1 > + { namesleft #1 > + { ", " * t * } + { numnames #2 > + { "," * } + 'skip$ + if$ + t "others" = + { " et~al." * } + { " and " * t * } + if$ + } + if$ + } + 't + if$ + nameptr #1 + 'nameptr := + namesleft #1 - 'namesleft := + } + while$ +} + +FUNCTION {format.authors} +{ author empty$ + { "" } + { author format.names } + if$ +} + +FUNCTION {format.key} +{ empty$ + { key field.or.null } + { "" } + if$ +} + +FUNCTION {format.editors} +{ editor empty$ + { "" } + { editor format.names + editor num.names$ #1 > + { " (eds.)" * } + { " (ed.)" * } + if$ + } + if$ +} + +FUNCTION {format.editors.extra} +{ editor empty$ + { "" } + { editor format.ed.names + editor num.names$ #1 > + { " (eds.)" * } + { " (ed.)" * } + if$ + } + if$ +} + +FUNCTION {format.title} +{ title empty$ + { "" } + { "`" title "'" * * } + if$ +} + +FUNCTION {n.dashify} +{ 't := + "" + { t empty$ not } + { t #1 #1 substring$ "-" = + { t #1 #2 substring$ "--" = not + { "--" * + t #2 global.max$ substring$ 't := + } + { { t #1 #1 substring$ "-" = } + { "-" * + t #2 global.max$ substring$ 't := + } + while$ + } + if$ + } + { t #1 #1 substring$ * + t #2 global.max$ substring$ 't := + } + if$ + } + while$ +} + +FUNCTION {first.page.number} +{ 't := + "" + { t "" = + { #0 } + { t #1 #1 substring$ "-" = not } + if$ + } + { t #1 #1 substring$ * + t #2 global.max$ substring$ 't := + } + while$ +} + +FUNCTION {format.btitle} +{ title emphasize +} + +FUNCTION {tie.or.space.connect} +{ duplicate$ text.length$ #3 < + { "~" } + { " " } + if$ + swap$ * * +} + +FUNCTION {either.or.check} +{ empty$ + 'pop$ + { "can't use both " swap$ * " fields in " * cite$ * warning$ } + if$ +} + +FUNCTION {format.bvolume} +{ volume empty$ + { "" } + { "Vol." volume tie.or.space.connect + series empty$ + 'skip$ + { " of " * series emphasize * } + if$ + "volume and number" number either.or.check + } + if$ +} + +FUNCTION {format.number.series} +{ volume empty$ + { number empty$ + { series field.or.null } + { output.state mid.sentence = + { "No." } + { "No." } + if$ + number tie.or.space.connect + series empty$ + { "there's a number but no series in " cite$ * warning$ } + { " in " * series * } + if$ + } + if$ + } + { "" } + if$ +} + +FUNCTION {format.edition} +{ edition empty$ + { "" } + { output.state mid.sentence = + { edition "l" change.case$ " edition" * } + { edition "t" change.case$ " edition" * } + if$ + } + if$ +} + +INTEGERS { multiresult } + +FUNCTION {multi.page.check} +{ 't := + #0 'multiresult := + { multiresult not + t empty$ not + and + } + { t #1 #1 substring$ + duplicate$ "-" = + swap$ duplicate$ "," = + swap$ "+" = + or or + { #1 'multiresult := } + { t #2 global.max$ substring$ 't := } + if$ + } + while$ + multiresult +} + +FUNCTION {format.pages} +{ pages empty$ + { "" } + { pages multi.page.check + { "pp." pages n.dashify tie.or.space.connect } + { "p." pages tie.or.space.connect } + if$ + } + if$ +} + +FUNCTION {format.page} +{ pages empty$ + { "" } + { "p.~" pages first.page.number * } + if$ +} + +FUNCTION {format.vol.num.pages} +{ volume field.or.null + volume empty$ + 'skip$ + { boldface } + if$ + number empty$ + 'skip$ + { "(" number * ")" * * + volume empty$ + { "there's a number but no volume in " cite$ * warning$ } + 'skip$ + if$ + } + if$ + pages empty$ + 'skip$ + { duplicate$ empty$ + { pop$ format.pages } + { ", " * pages n.dashify * } + if$ + } + if$ +} + +FUNCTION {format.vol.num.page} +{ volume field.or.null + volume empty$ + 'skip$ + { boldface } + if$ + number empty$ + 'skip$ + { "(" number * ")" * * + volume empty$ + { "there's a number but no volume in " cite$ * warning$ } + 'skip$ + if$ + } + if$ + pages empty$ + 'skip$ + { duplicate$ empty$ + { pop$ format.pages } + { ", " * pages first.page.number * } + if$ + } + if$ +} + +FUNCTION {format.chapter.pages} +{ chapter empty$ + 'format.pages + { type empty$ + { "Chapt." } + { type "l" change.case$ } + if$ + chapter tie.or.space.connect + pages empty$ + 'skip$ + { ", " * format.pages * } + if$ + } + if$ +} + +FUNCTION {format.in.ed.booktitle} +{ booktitle empty$ + { "" } + { editor empty$ + { "In: " booktitle emphasize * } + { "In: " format.editors.extra * ": " * booktitle emphasize * } + if$ + } + if$ +} + +FUNCTION {format.in.booktitle.or.series} +{ booktitle empty$ + { series empty$ + { "" } + { "In: " series emphasize * } + if$ + } + { editor empty$ + { "In: " booktitle emphasize * } + { "In: " format.editors.extra * ": " * booktitle emphasize * } + if$ + } + if$ +} + +FUNCTION {format.thesis.type} +{ type empty$ + 'skip$ + { pop$ + type "t" change.case$ + } + if$ +} + +FUNCTION {format.tr.number} +{ type empty$ + { "Technical Report" } + 'type + if$ + number empty$ + { "t" change.case$ } + { number tie.or.space.connect } + if$ +} + +FUNCTION {format.article.crossref} +{ "In" + " \cite{" * crossref * "}" * +} + +FUNCTION {format.book.crossref} +{ volume empty$ + { "empty volume in " cite$ * "'s crossref of " * crossref * warning$ + "In " + } + { "Vol." volume tie.or.space.connect + " of " * + } + if$ + "\cite{" * crossref * "}" * +} + +FUNCTION {format.incoll.inproc.crossref} +{ "In" + " \cite{" * crossref * "}" * +} + +FUNCTION {article} +{ output.bibitem + format.authors "author" output.check + author format.key output + output.year.check + format.title "title" output.check + new.block + crossref missing$ + { journal emphasize "journal" output.check.extra + format.vol.num.pages output.extra + } + { format.article.crossref output.nonnull + format.pages output + } + if$ + new.block + note output + fin.entry +} + +FUNCTION {book} +{ output.bibitem + author empty$ + { format.editors "author and editor" output.check + editor format.key output + } + { format.authors output.nonnull + crossref missing$ + { "author and editor" editor either.or.check } + 'skip$ + if$ + } + if$ + output.year.check + format.btitle "title" output.check + crossref missing$ + { format.bvolume output + format.number.series output + new.block + address empty$ + 'skip$ + { address ": " * output + after.colon 'output.state := + } + if$ + publisher "publisher" output.check.extra + } + { new.block + format.book.crossref output.nonnull + } + if$ + format.edition output + new.block + note output + fin.entry +} + +FUNCTION {booklet} +{ output.bibitem + format.authors output + author format.key output + output.year.check + format.btitle "title" output.check + new.block + howpublished output + address output + new.block + note output + fin.entry +} + +FUNCTION {inbook} +{ output.bibitem + author empty$ + { format.editors "author and editor" output.check + editor format.key output + } + { format.authors output.nonnull + crossref missing$ + { "author and editor" editor either.or.check } + 'skip$ + if$ + } + if$ + output.year.check + format.btitle "title" output.check + crossref missing$ + { format.bvolume output + format.chapter.pages "chapter and pages" output.check + format.number.series output + new.block + address empty$ + 'skip$ + { address ": " * output + after.colon 'output.state := + } + if$ + publisher "publisher" output.check.extra + } + { format.chapter.pages "chapter and pages" output.check + new.block + format.book.crossref output.nonnull + } + if$ + format.edition output + new.block + note output + fin.entry +} + +FUNCTION {incollection} +{ output.bibitem + format.authors "author" output.check + author format.key output + output.year.check + format.title "title" output.check + new.block + crossref missing$ + { format.in.ed.booktitle "booktitle" output.check + format.bvolume output + format.number.series output + new.block + address empty$ + 'skip$ + { address ": " * output + after.colon 'output.state := + } + if$ + publisher "publisher" output.check.extra + format.edition output + format.chapter.pages output + } + { format.incoll.inproc.crossref output.nonnull + format.chapter.pages output + } + if$ + new.block + note output + fin.entry +} + +FUNCTION {inproceedings} +{ output.bibitem + format.authors "author" output.check + author format.key output + output.year.check + format.title "title" output.check + new.block + crossref missing$ + { format.in.booktitle.or.series "booktitle or series" output.check + format.bvolume output + new.sentence + address output + format.pages output + } + { format.incoll.inproc.crossref output.nonnull + format.pages output + } + if$ + publisher output + new.block + note output + fin.entry +} + +FUNCTION {conference} { inproceedings } + +FUNCTION {manual} +{ output.bibitem + format.authors output + author format.key output + output.year.check + format.title "title" output.check + new.block + organization output + address output + format.edition output + new.block + note output + fin.entry +} + +FUNCTION {mastersthesis} +{ output.bibitem + format.authors "author" output.check + author format.key output + output.year.check + format.title "title" output.check + new.block + "Master's thesis" format.thesis.type output.nonnull + school "school" output.check + address output + new.block + note output + fin.entry +} + +FUNCTION {misc} +{ output.bibitem + format.authors output + author format.key output + output.year.check + format.title output + new.block + howpublished output + new.block + note output + fin.entry +} + +FUNCTION {phdthesis} +{ output.bibitem + format.authors "author" output.check + author format.key output + output.year.check + format.title "title" output.check + new.block + "Ph.D. thesis" format.thesis.type output.nonnull + school "school" output.check + address output + new.block + note output + fin.entry +} + +FUNCTION {proceedings} +{ output.bibitem + format.editors output + editor format.key output + output.year.check + format.title "title" output.check + format.bvolume output + format.number.series output + new.block + address empty$ + 'skip$ + { address ": " * output + after.colon 'output.state := + } + if$ + organization output.extra + publisher output + new.block + note output + fin.entry +} + +FUNCTION {techreport} +{ output.bibitem + format.authors "author" output.check + author format.key output + output.year.check + format.title "title" output.check + new.block + format.tr.number output.nonnull + institution "institution" output.check + address output + new.block + note output + fin.entry +} + +FUNCTION {unpublished} +{ output.bibitem + format.authors "author" output.check + author format.key output + output.year.check + format.title "title" output.check + new.block + note "note" output.check + fin.entry +} + +FUNCTION {default.type} { misc } + +MACRO {jan} {"Jan."} + +MACRO {feb} {"Feb."} + +MACRO {mar} {"Mar."} + +MACRO {apr} {"Apr,"} + +MACRO {may} {"May"} + +MACRO {jun} {"June"} + +MACRO {jul} {"July"} + +MACRO {aug} {"Aug."} + +MACRO {sep} {"Sept."} + +MACRO {oct} {"Oct."} + +MACRO {nov} {"Nov."} + +MACRO {dec} {"Dec."} + +READ + +FUNCTION {sortify} +{ purify$ + "l" change.case$ +} + +INTEGERS { len } + +FUNCTION {chop.word} +{ 's := + 'len := + s #1 len substring$ = + { s len #1 + global.max$ substring$ } + 's + if$ +} + +FUNCTION {format.lab.names} +{ 's := + s #1 "{vv~}{ll}" format.name$ + s num.names$ duplicate$ + #2 > + { pop$ " et~al." * } + { #2 < + 'skip$ + { s #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" = + { " et~al." * } + { " and " * s #2 "{vv~}{ll}" format.name$ * } + if$ + } + if$ + } + if$ +} + +FUNCTION {author.key.label} +{ author empty$ + { key empty$ + { cite$ #1 #3 substring$ } + 'key + if$ + } + { author format.lab.names } + if$ +} + +FUNCTION {author.editor.key.label} +{ author empty$ + { editor empty$ + { key empty$ + { cite$ #1 #3 substring$ } + 'key + if$ + } + { editor format.lab.names } + if$ + } + { author format.lab.names } + if$ +} + +FUNCTION {editor.key.label} +{ editor empty$ + { key empty$ + { cite$ #1 #3 substring$ } + 'key + if$ + } + { editor format.lab.names } + if$ +} + +FUNCTION {calc.label} +{ type$ "book" = + type$ "inbook" = + or + 'author.editor.key.label + { type$ "proceedings" = + 'editor.key.label + 'author.key.label + if$ + } + if$ + "\protect\citeauthoryear{" swap$ * "}{" + * + year field.or.null purify$ #-1 #4 substring$ + * + 'label := +} + +FUNCTION {sort.format.names} +{ 's := + #1 'nameptr := + "" + s num.names$ 'numnames := + numnames 'namesleft := + { namesleft #0 > } + { nameptr #1 > + { " " * } + 'skip$ + if$ + s nameptr "{vv{ } }{ll{ }}{ f{ }}{ jj{ }}" format.name$ 't := + nameptr numnames = t "others" = and + { "et al" * } + { t sortify * } + if$ + nameptr #1 + 'nameptr := + namesleft #1 - 'namesleft := + } + while$ +} + +FUNCTION {sort.format.title} +{ 't := + "A " #2 + "An " #3 + "The " #4 t chop.word + chop.word + chop.word + sortify + #1 global.max$ substring$ +} + +FUNCTION {author.sort} +{ author empty$ + { key empty$ + { "to sort, need author or key in " cite$ * warning$ + "" + } + { key sortify } + if$ + } + { author sort.format.names } + if$ +} + +FUNCTION {author.editor.sort} +{ author empty$ + { editor empty$ + { key empty$ + { "to sort, need author, editor, or key in " cite$ * warning$ + "" + } + { key sortify } + if$ + } + { editor sort.format.names } + if$ + } + { author sort.format.names } + if$ +} + +FUNCTION {editor.sort} +{ editor empty$ + { key empty$ + { "to sort, need editor or key in " cite$ * warning$ + "" + } + { key sortify } + if$ + } + { editor sort.format.names } + if$ +} + +FUNCTION {presort} +{ calc.label + label sortify + " " + * + type$ "book" = + type$ "inbook" = + or + 'author.editor.sort + { type$ "proceedings" = + 'editor.sort + 'author.sort + if$ + } + if$ + #1 entry.max$ substring$ + 'sort.label := + sort.label + * + " " + * + title field.or.null + sort.format.title + * + #1 entry.max$ substring$ + 'sort.key$ := +} + +ITERATE {presort} + +SORT % by label, sort.label, title---for final label calculation + +STRINGS { last.label next.extra } + +INTEGERS { last.extra.num } + +FUNCTION {initialize.extra.label.stuff} +{ #0 int.to.chr$ 'last.label := + "" 'next.extra := + #0 'last.extra.num := +} + +FUNCTION {forward.pass} +{ last.label label = + { last.extra.num #1 + 'last.extra.num := + last.extra.num int.to.chr$ 'extra.label := + } + { "a" chr.to.int$ 'last.extra.num := + "" 'extra.label := + label 'last.label := + } + if$ +} + +FUNCTION {reverse.pass} +{ next.extra "b" = + { "a" 'extra.label := } + 'skip$ + if$ + label extra.label * "}" * 'label := + extra.label 'next.extra := +} + +EXECUTE {initialize.extra.label.stuff} + +ITERATE {forward.pass} + +REVERSE {reverse.pass} + +FUNCTION {bib.sort.order} +{ sort.label + " " + * + year field.or.null sortify + * + " " + * + title field.or.null + sort.format.title + * + #1 entry.max$ substring$ + 'sort.key$ := +} + +ITERATE {bib.sort.order} + +SORT % by sort.label, year, title---giving final bibliography order + +FUNCTION {begin.bib} +{ preamble$ empty$ + 'skip$ + { preamble$ write$ newline$ } + if$ + "\begin{thebibliography}{}" write$ newline$ +} + +EXECUTE {begin.bib} + +EXECUTE {init.state.consts} + +ITERATE {call.type$} + +FUNCTION {end.bib} +{ newline$ + "\end{thebibliography}" write$ newline$ +} + +EXECUTE {end.bib} + + diff --git a/papers/cfrontend_new/kluwer.cls b/papers/cfrontend_new/kluwer.cls new file mode 100755 index 0000000..ab443f3 --- /dev/null +++ b/papers/cfrontend_new/kluwer.cls @@ -0,0 +1,2873 @@ +%% +%% This is file `kluwer.cls', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% kluwer.dtx (with options: `head') +%% klumac.sty (with options: `head') +%% klu11.clo (with options: `head') +%% klulist.sty (with options: `head') +%% kluopen.sty (with options: `head') +%% kluedit.sty (with options: `head') +%% klutab.sty (with options: `head') +%% klufloa.sty (with options: `head') +%% klunote.sty (with options: `head') +%% kluref.sty (with options: `head') +%% klumath.sty (with options: `head') +%% klusec.sty (with options: `head') +%% kluwer.dtx (with options: `neck') +%% klumac.sty (with options: `neck') +%% klumac.sty (with options: `main') +%% klu11.clo (with options: `main') +%% klulist.sty (with options: `main') +%% kluopen.sty (with options: `main') +%% kluedit.sty (with options: `main') +%% klutab.sty (with options: `main') +%% klufloa.sty (with options: `main') +%% klunote.sty (with options: `main') +%% kluref.sty (with options: `main') +%% klumath.sty (with options: `main') +%% klusec.sty (with options: `main') +%% kluwer.dtx (with options: `tail') +%% +%% IMPORTANT NOTICE: +%% +%% For the copyright see the source file. +%% +%% Any modified versions of this file must be renamed +%% with new filenames distinct from kluwer.cls. +%% +%% For distribution of the original source see the terms +%% for copying and modification in the file kluwer.dtx klumac.sty klu11.clo klulist.sty kluopen.sty kluedit.sty klutab.sty klufloa.sty klunote.sty kluref.sty klumath.sty klusec.sty kluwer.dtx klumac.sty klumac.sty klu11.clo klulist.sty kluopen.sty kluedit.sty klutab.sty klufloa.sty klunote.sty kluref.sty klumath.sty klusec.sty kluwer.dtx. +%% +%% This generated file may be distributed as long as the +%% original source files, as listed above, are part of the +%% same distribution. (The sources need not necessarily be +%% in the same archive or directory.) +\def\filedate{2000/04/29} +\def\kluclassname{kluwer} +\def\kluclassversion{1.3} % option kaplist turned on for 1.2 +\def\klujnlname{none} +\NeedsTeXFormat{LaTeX2e} +\ProvidesClass{kluwer}[\filedate\space \kluclassversion\space + Kluwer base document class] +\newcommand\@ptsize{} +\newcommand\@pttensize{1} +\newif\if@restonecol +\newif\if@openright + +\DeclareOption{a4paper} + {\setlength\paperheight {297mm}% + \setlength\paperwidth {210mm}} +\DeclareOption{a5paper} + {\setlength\paperheight {210mm}% + \setlength\paperwidth {148mm}} +\DeclareOption{b5paper} + {\setlength\paperheight {250mm}% + \setlength\paperwidth {176mm}} +\DeclareOption{letterpaper} + {\setlength\paperheight {11in}% + \setlength\paperwidth {8.5in}} +\DeclareOption{legalpaper} + {\setlength\paperheight {14in}% + \setlength\paperwidth {8.5in}} +\DeclareOption{executivepaper} + {\setlength\paperheight {10.5in}% + \setlength\paperwidth {7.25in}} +\DeclareOption{landscape} + {\setlength\@tempdima {\paperheight}% + \setlength\paperheight {\paperwidth}% + \setlength\paperwidth {\@tempdima}} +\DeclareOption{9pt}{\renewcommand\@pttensize{}\renewcommand\@ptsize{9}} +\DeclareOption{10pt}{\renewcommand\@ptsize{0}} +\DeclareOption{11pt}{\renewcommand\@ptsize{1}} +\DeclareOption{12pt}{\renewcommand\@ptsize{2}} +\DeclareOption{oneside}{\@twosidefalse \@mparswitchfalse} +\DeclareOption{twoside}{\@twosidetrue \@mparswitchtrue} +\DeclareOption{openright}{\@openrighttrue} +\DeclareOption{draft}{\setlength\overfullrule{5pt}} +\DeclareOption{final}{\setlength\overfullrule{0pt}} +\DeclareOption{onecolumn}{\@twocolumnfalse} +\DeclareOption{twocolumn}{\@twocolumntrue} +\ExecuteOptions{a4paper,11pt,twoside,onecolumn,final,openright} + + + + +\font\@klusymfont=cmr10 +\DeclareOption{klusym}{\font\@klusymfont=klusym10 } +\newif\if@kaplist +\DeclareOption{kaplist}{\@kaplisttrue} +\newif\if@margspec +\DeclareOption{margspec}{\@margspectrue} +\newif\if@copyrighthead \@copyrightheadfalse +\newif\if@kapidenthead \@kapidentheadfalse +\newif\if@noid \@noidfalse +\DeclareOption{copyrighthead}{\@copyrightheadtrue} +\DeclareOption{kapidenthead}{\@kapidentheadtrue} +\DeclareOption{noid}{\@noidtrue} +\newif\if@numreferences +\DeclareOption{namedreferences}{\@numreferencesfalse} +\DeclareOption{numreferences}{\@numreferencestrue} +\DeclareOption{openbib}{} +\ExecuteOptions{namedreferences} +\let\@EndKlumathook\@empty +\def\AtEndKluMath{\g@addto@macro\@EndKlumathook} + +\DeclareOption{leqno}{\AtEndKluMath{\varleqno}} +\DeclareOption{fleqn}{\AtEndKluMath{\varfleqn}} +\DeclareOption{mathsec}{% + \def\theequation{\arabic{section}.\arabic{equation}}} +\DeclareOption{mathchap}{% + \def\theequation{\arabic{chapter}.\arabic{equation}}} +\newif\if@thms \@thmsfalse +\DeclareOption{thms}{\@thmstrue } +\DeclareOption{secthm}{\AtEndKluMath{\if@thms + \renewcommand{\thethm}{\thesection.\arabic{thm}.}% + \renewcommand{\thecrit}{\thesection.\arabic{crit}.}% + \renewcommand{\therem}{\thesection.\arabic{rem}.}% + \renewcommand{\theNote}{\thesection.\arabic{Note}.}% + \renewcommand{\thesumm}{\thesection.\arabic{summ}.}% + \renewcommand{\thecase}{\thesection.\arabic{case}.}% + \fi + }} +\newif\if@chapterdef \@chapterdeffalse +\DeclareOption{chapter}{\@chapterdeftrue } + + +\ProcessOptions % including options for modules + + +\IfFileExists{amssymb.sty}{\RequirePackage[psamsfonts]{amssymb}% + \global\font\smallmsa=msam7 + \gdef\Register{$^{\mbox{\smallmsa\char114}}$~}}{} +\IfFileExists{wasysym.sty}{\RequirePackage{wasysym}}{% + \IfFileExists{wasysym.tex}{\input{wasysym}}{}} +\def\I{{\bf I}} +\newcommand\iduaal{\overline{\I}} +\let\forces\Vdash +\newcommand\rrestrict{\hbox{$\mid$ \kern-5pt \raise3.6pt\hbox{$ + \scriptscriptstyle \backslash$}}} +\newcommand\restrict{\mathrel{\mathpalette\rrestrict{}}} +\let\diamond\lozenge +\newcommand\concat{\mathrel{\raise1pt\hbox{$\!\!^\frown\!\!$}}} +\newcommand\lh{\mathop\mathrm{lh}} +\newcommand\depth{\mathop\mathrm{depth}} +\newcommand\dom{\mathop\mathrm{dom}} +\newcommand\range{\mathop\mathrm{range}} +\newcommand\mapright[1]{\smash{\mathop{\longrightarrow}\limits^{#1}}} +\newcommand\mapdown[1]{\big\downarrow + \rlap{$\vcenter{\hbox{$\scriptstyle#1$}}$}} +\newcommand{\dC}{C \! \! \! \! {\scriptscriptstyle {}^{{}_|}}\ } +\newcommand{\dL}{I \! \! L} +\newcommand{\dE}{I \! \! E} +\newcommand{\dF}{I \! \! F} +\newcommand{\dP}{I \! \! P} +\newcommand{\dN}{I \! \! N} +\newcommand{\dR}{I \! \! R} +\newcommand{\dZ}{Z \! \! \! Z} +\newcommand{\dQ}{Q \! \! \! \! {\scriptscriptstyle {}^|}\ } +\newcommand{\nequiv}{\mathrel{\setbox0\hbox{$\equiv$}% + \rlap{\hbox{$\equiv$}}\hbox to \wd0{\hfil $/$\hfil}}} +\newcommand{\lsim}{\mathrel{\rlap{\raise -.3ex\hbox{${\scriptstyle\sim}$}}% + \raise .6ex\hbox{${\scriptstyle <}$}}}% +\newcommand{\gsim}{\mathrel{\rlap{\raise -.3ex\hbox{${\scriptstyle\sim}$}}% + \raise .6ex\hbox{${\scriptstyle >}$}}}% +\newcommand{\logr}{\mathrel{\rlap{\raise -.3ex\hbox{${\scriptstyle <}$}}% + \raise .6ex\hbox{${\scriptstyle >}$}}}% +\newcommand{\grlo}{\mathrel{\rlap{\raise -.3ex\hbox{${\scriptstyle >}$}}% + \raise .6ex\hbox{${\scriptstyle <}$}}}% +\newcommand{\oast}{\setbox0\hbox{$\odot$}% + \rlap{\hbox to \wd0{\hfil$\ast$\hfil}}\box0} +\newcommand{\res}{\oalign{\hbox{$\grave{}$\kern-3pt$\mid$}}} +\newcommand{\dres}{\mid \! \res} +\newcommand{\bigo}[1]{\setbox0\hbox{$\bigcirc$}% + \rlap{\raise .2ex\hbox to \wd0{\hfil ${\scriptscriptstyle + #1}$\hfil}}\box0} +\newcommand{\Res}[1]{\mathop{\hbox{Res}}\limits_{\scriptscriptstyle #1}} +\newcommand{\down}[1]{\raise -1ex\hbox{{$\scriptstyle #1$}}} +\newcount\@cla +\newcount\@clb +\hyphenation{equiv-a-lent equiv-a-lent-ly sat-is-fy sat-is-fies + sat-is-fied} +\newcommand\fn{\hspace*{14pt} \= \kill} +\newcommand\mc{\multicolumn} +\newcommand{\dummy}[1]{} +\def\today{\ifcase\month\or January\or February\or March\or April\or + May\or June\or July\or August\or September\or October\or November\or + December\fi \space\number\day, \number\year} +\def\TODAY{\number\day/\ifcase\month\or 01\or 02\or 03\or 04\or 05\or + 06\or 07\or 08\or 09\or 10\or 11\or 12\fi/\number\year} +\def\timenow{% + \@tempcnta=\time \divide\@tempcnta by 60 \number\@tempcnta:\multiply + \@tempcnta by 60 \@tempcntb=\time \advance\@tempcntb by -\@tempcnta + \ifnum\@tempcntb <10 0\number\@tempcntb\else\number\@tempcntb\fi} +\def\numtoword#1{\ifcase#1\or one\or two\or three\or four\or + five\or six\or seven\or eight\or nine\or ten\or eleven\or twelve\or + thirteen\or fourteen\or fifteen\or sixteen\or seventeen\or + eighteen\or nineteen\or twenty\fi} +\def\NUMTOWORD#1{\ifcase#1\or ONE\or TWO\or THREE\or FOUR\or + FIVE\or SIX\or SEVEN\or EIGHT\or NINE\or TEN\or ELEVEN\or TWELVE\or + THIRTEEN\or FOURTEEN\or FIFTEEN\or SIXTEEN\or SEVENTEEN\or + EIGHTEEN\or NINETEEN\or TWENTY\fi} + +\def\ifempty#1#2#3{\def\inner{#1}\ifx\inner\empty + #2\else #3\fi } +\def\ifdef#1{\edef\tempa{\expandafter\@gobble\string #1}% + \expandafter\expandafter\expandafter\ifx\expandafter\csname + \tempa \endcsname\relax + \let\next\nosw \else \let\next=\yessw \fi \next} +\def\nosw{\iffalse} +\def\yessw{\iftrue} +\newif\ifklaar +\newbox\bdj +\def\onestep#1{\ifklaar\else + \if#1){)}\klaartrue\else + \if#1.{.}\klaartrue\else + \if#1]{]}\klaartrue\else + \if#1-{--}\klaartrue\else + \if#1*{*}\klaartrue\else + #1% + \fi\fi\fi\fi\fi + \fi} +\def\subspitem#1{\scan#1\end} +\def\spitem#1 {% + \def\scan##1##2\end{\def\aux{##1}% + \ifklaar\global\setbox\bdj=\hbox{##1##2\space}\else + \ifx\aux\empty \else \def\aux{##2}\onestep{##1}% + \ifx\aux\empty \else \scan##2\end \fi \fi \fi}% + \global\setbox\bdj\hbox{}% + \klaarfalse\expandafter\item[\subspitem{#1}]% + \unhbox\bdj} +\font\genacc=cmr10 +\def\genaccent#1#2#3#4#5{\protect\@genaccent{#1}{#2}{#3}{#4}{#5}} +\def\@genaccent#1#2#3#4#5{% + \leavevmode\setbox0=\hbox{#3}% + \vbox{\offinterlineskip + \ifempty{#1}{}{%\else + \hbox to\wd0{\hss\genacc \char#1\hss}}% + \ifempty{#4}{\kern -.8ex}{\kern #4}% + \vbox to\ht0{\copy0\vss}% + \vtop{\null\vbox to\dp0{\vss}% + \ifempty{#2}{}{%\else + \ifempty{#5}{\kern .2ex}{\kern#5}% + \hbox to \wd0{\hss \genacc\char #2\hss}}% + }}} +\renewcommand\.[1]{\genaccent{95}{}{#1}{}{}} +\newcommand\BlackBox{\hbox{\@klusymfont B}~} +\newcommand\EmptyBox{\hbox{\@klusymfont E}~} +\newcommand\HstripeBox{\hbox{\@klusymfont H}~} +\newcommand\VstripeBox{\hbox{\@klusymfont V}~} +\newcommand\LstripeBox{\hbox{\@klusymfont L}~} +\newcommand\RstripeBox{\hbox{\@klusymfont R}~} +\newcommand\UpCrossBox{\hbox{\@klusymfont U}~} +\newcommand\DiagCrossBox{\hbox{\@klusymfont D}~} +\def\cb{\@ifnextchar[{\@cbone}{\@cbone[8pc]}} +\def\@cbone[#1]#2{{\setbox0\hbox{#2}% + \ifdim\wd0 >#1 \parbox[t]{#1}{#2}\else #2\fi}} +\def\nbox#1#2#3#4#5#6{\begingroup\setbox0\hbox{0}% + \ifempty{#1}{\hfil #2}{\hbox to #1\wd0{\hfil #2}}% + \ifempty{#3}{\hbox{#4}}{\hbox to #3\wd0{\hfil #4\hfil }}% + \ifempty{#5}{#6 \hfil}{\hbox to #5\wd0{#6\hfil }}% + \endgroup} +\newif\ifkern@mathmode \kern@mathmodefalse +\def\charkerncharspace{\kern 0.5ex} +\def\charkernwordspace{\kern 0.5em\penalty 10} +\let\charkerncommand\uppercase +\def\@kap@tfor#1:=#2\do#3{\ifempty{#1}{}{% + \@tforloop#2\@nil\@nil\@@#1{#3}}} +\def\charkern#1{% + \ifempty{#1}{}{%else + \begingroup + \def\test##1##2!!!!{\def\@tempa{##2}}\test#1!!!!% + \ifx\@tempa\empty \edef\@@kc{#1}\else \def\@@kc{#1}\fi + \def\c@@k{@s@e@v@y}% + \def\ck@@##1 @s@e@v@y\@@ck{\def\@@kc{##1}}% + \def\ck@##1 ##2\@@ck{\def\@kc{##1}\def\@@kc{##2}}% + \def\iterate{\expandafter\expandafter\expandafter\ck@ + \expandafter\@@kc\space @s@e@v@y\@@ck + \expandafter\@kernword\expandafter{\@kc}% + \ifx\@@kc\c@@k + \let\next\relax + \else + \expandafter\ck@@\@@kc\@@ck + \let\next\iterate\charkernwordspace + \fi\next}\iterate + \endgroup + }} + +\def\@kernword#1{\def\d@ll@rm@th{$}\@kap@tfor\@nextchar:=#1\do{% + \ifx\@nextchar\d@ll@rm@th + \ifkern@mathmode + \kern@mathmodefalse + $\kern@math$% + \else + \kern@mathmodetrue + \xdef\kern@math{}% + \fi + \else + \ifkern@mathmode + \begingroup + \def\protect{\noexpand}% + \xdef\kern@math{\kern@math\@nextchar}% + \endgroup + \else + \charkerncommand\expandafter{\@nextchar}\charkerncharspace + \fi + \fi +}} + +\newcount\tracingkluwer +\def\kludebug#1{\relax\ifcase\tracingkluwer \or + \wlog{kap: #1}\or \typeout{kap: #1}\else + \immediate\wlog{kap*: #1}\typeout{kap: #1}\fi} +\global\tracingkluwer=3 +\def\kluverbatim{\par\begingroup\vbox \bgroup\trivlist + \item\relax \vskip\parskip + \rightskip\z@skip \parindent\z@ + \parfillskip\@flushglue \parskip0pt \@@par \@tempswafalse + \def\par{\if@tempswa \leavevmode\null\@@par\penalty\interlinepenalty + \else \@tempswatrue \ifhmode\@@par\penalty\interlinepenalty\fi \fi} + \let\do\@makeother \catcode`\|=0 + \obeylines \verbatim@font \@noligs \dospecials \catcode`\%=14 + \frenchspacing\@vobeyspaces + \everypar \expandafter{\the\everypar \unpenalty }} +\def\endkluverbatim{\endtrivlist\egroup\endgroup} +\renewcommand\normalsize{% + \@setfontsize\normalsize\@xipt{13}% + \abovedisplayskip 10\p@ \@plus 2\p@ \@minus5\p@ + \abovedisplayshortskip \z@ \@plus 3\p@ + \belowdisplayshortskip 6\p@ \@plus 3\p@ \@minus3\p@ + \belowdisplayskip \abovedisplayskip + \let\@listi\@listI} +\normalsize +\newcommand\small{% + \@setfontsize\small\@xpt\@xiipt + \abovedisplayskip 9\p@ \@plus3\p@ \@minus4\p@ + \abovedisplayshortskip \z@ \@plus2\p@ + \belowdisplayshortskip 5\p@ \@plus2\p@ \@minus2\p@ + \def\@listi{\leftmargin\leftmargini + \topsep 4\p@ \@plus2\p@ \@minus2\p@ + \parsep 2\p@ \@plus\p@ \@minus\p@ + \itemsep \parsep}% + \belowdisplayskip \abovedisplayskip +} +\newcommand\footnotesize{% + \@setfontsize\footnotesize\@ixpt\@xipt + \abovedisplayskip 6\p@ \@plus2\p@ \@minus4\p@ + \abovedisplayshortskip \z@ \@plus\p@ + \belowdisplayshortskip 3\p@ \@plus\p@ \@minus2\p@ + \def\@listi{\leftmargin\leftmargini + \topsep 3\p@ \@plus\p@ \@minus\p@ + \parsep 2\p@ \@plus\p@ \@minus\p@ + \itemsep \parsep}% + \belowdisplayskip \abovedisplayskip +} +\newcommand\scriptsize{\@setfontsize\scriptsize\@viiipt{9.5}} +\newcommand\little{\@setfontsize\little\@viipt\@viiipt} +\newcommand\tiny{\@setfontsize\tiny\@vipt\@viipt} +\newcommand\large{\@setfontsize\large\@xiipt{14}} +\newcommand\Large{\@setfontsize\Large\@xivpt{18}} +\newcommand\LARGE{\@setfontsize\LARGE\@xviipt{22}} +\newcommand\huge{\@setfontsize\huge\@xxpt{25}} +\newcommand\Huge{\@setfontsize\Huge\@xxvpt{30}} +\setlength\hoffset{-1in} +\setlength\voffset{0pt} +\setlength\parindent {14\p@} +\setlength\headheight{12\p@} +\setlength\headsep {13\p@} +\setlength\topskip {10\p@} +\setlength\footskip {27.5\p@} +\setlength\marginparsep{10pt} +\setlength\marginparpush{5\p@} +\setlength\maxdepth {.5\topskip} +\setlength\@maxdepth\maxdepth +\setlength\columnsep{10pt} +\setlength\columnseprule{0pt} +\setlength\fboxsep{3pt} +\setlength\fboxrule{.4pt} +\newdimen\id@boxheight +\AtBeginDocument{% + \setlength\@tempdima{\paperwidth}% + \addtolength\@tempdima{-\textwidth}% + \divide\@tempdima by 2 + \setlength\@tempdimb\marginparwidth + \addtolength\@tempdimb\marginparsep + \addtolength\@tempdimb{2pc}% + \ifdim \@tempdima <\@tempdimb + \@settopoint\@tempdimb + \GenericError{Pointsize}{Pointsize Error: Marginpars disabled}{}{You made + your \string\textwidth\space (\the\textwidth) and + \string\marginparwidth (\the\marginparwidth) too wide.\MessageBreak + The allowed value for margin space: (\the\@tempdima). Needed value: + (\the\@tempdimb).\MessageBreak + This is not enough, + so I will set \string\marginparwidth\space to 0pt.\MessageBreak + Let's hope that fixes it. + }% + \marginparwidth \z@ + \marginparsep \z@ + \fi + \ifdim \@tempdima <2pc + \@tempdimb=\paperwidth + \advance\@tempdimb by -4pc + \@settopoint\@tempdimb + \GenericError{Pointsize}{Pointsize Error: Invalid sizes given}{}{You + made your \string\textwidth\space (\the\textwidth) + wider than the available total\MessageBreak + (Which is: \the\@tempdimb). Please press X and try again. + }% + \fi + \oddsidemargin \@tempdima + \evensidemargin \@tempdima + \setlength\@tempdima{\paperheight} + \addtolength\@tempdima{-\footskip} + \addtolength\@tempdima{-\headheight} + \addtolength\@tempdima{-\headsep} + \setlength\@tempdimb{\@tempdima} + \addtolength\@tempdima{-\textheight} + \divide\@tempdima by 2 + \ifdim \@tempdima <2pc + \advance\@tempdimb by -4pc + \@settopoint\@tempdimb + \GenericError{Pointsize}{Pointsize Error: Invalid sizes given}{}{You + made your \string\textheight\space (\the\textheight) + more than the available total.\MessageBreak + (Which is: \the\@tempdimb). Please press X and try again. + }% + \fi + \setlength\topmargin{0pt} + \setlength\id@boxheight{\@tempdima} + \advance\id@boxheight by -2pc +} +\setlength\footnotesep{6.65\p@} +\setlength{\skip\footins}{9\p@ \@plus 4\p@ \@minus 2\p@} +\setlength\partopsep{2\p@ \@plus 1\p@ \@minus 1\p@} +\setlength{\leftmargini}{2em} +\setlength{\leftmarginii}{2.2em} +\setlength{\leftmarginiii}{1.87em} +\setlength{\leftmarginiv}{1.7em} +\setlength{\leftmarginv}{1em} +\setlength{\leftmarginvi}{1em} +\setlength{\labelsep}{.4em} +\setlength{\labelwidth}{\leftmargini} +\addtolength{\labelwidth}{-\labelsep} +\def\@listI{% + \leftmargin \leftmargini + \topsep 9\p@ \@plus 3\p@ \@minus 5\p@ + \partopsep 3\p@ \@plus 1\p@ \@minus 2\p@ + \itemsep 4.5\p@ \@plus 2\p@ \@minus 1\p@ + \parsep 4.5\p@ \@plus 2\p@ \@minus 1\p@ } +\def\@listii{% + \leftmargin \leftmarginii + \labelwidth \leftmarginii + \advance\labelwidth by -\labelsep + \topsep 4.5\p@ \@plus 2\p@ \@minus 1\p@ + \parsep 2\p@ \@plus 1\p@ \@minus 1\p@ + \itemsep \parsep} +\def\@listiii{% + \leftmargin \leftmarginiii + \labelwidth \leftmarginiii + \advance\labelwidth by -\labelsep + \topsep 2\p@ \@plus 1\p@ \@minus 1\p@ + \parsep \z@ + \partopsep 1\p@ \@plus 0\p@ \@minus 1\p@ + \itemsep \topsep} +\def\@listiv{% + \setlength{\leftmargin}{\leftmarginiv}% + \setlength{\labelwidth}{\leftmarginiv}% + \addtolength{\labelwidth}{-\labelsep}} +\def\@listv{% + \setlength{\leftmargin}{\leftmarginv}% + \setlength{\labelwidth}{\leftmarginv}% + \addtolength{\labelwidth}{-\labelsep}} +\def\@listvi{% + \setlength{\leftmargin}{\leftmarginvi}% + \setlength{\labelwidth}{\leftmarginvi}% + \addtolength{\labelwidth}{-\labelsep}} +\let\@listi\@listI +\@listi +\setlength\floatsep{12\p@ \@plus 2\p@ \@minus 2\p@} +\setlength\textfloatsep{20\p@ \@plus 2\p@ \@minus 4\p@} +\setlength\intextsep{12\p@ \@plus 2\p@ \@minus 2\p@} +\setlength\dblfloatsep{12\p@ \@plus 2\p@ \@minus 2\p@} +\setlength\dbltextfloatsep{20\p@ \@plus 2\p@ \@minus 4\p@} +\setlength\@fptop{0\p@ \@plus 1fil} +\setlength\@fpsep{8\p@ \@plus 2fil} +\setlength\@fpbot{0\p@ \@plus 1fil} +\setlength\@dblfptop{0\p@ \@plus 1fil} +\setlength\@dblfpsep{8\p@ \@plus 2fil} +\setlength\@dblfpbot{0\p@ \@plus 1fil} +\def\labelenumi{\arabic{enumi}.} % 1. +\def\theenumi{\arabic{enumi}} % 1 +\def\labelenumii{\alph{enumii})} % a) +\def\theenumii{\alph{enumii}} % a +\def\p@enumii{\theenumi} % 1a +\def\labelenumiii{\it\roman{enumiii})} % \it i) +\def\theenumiii{\roman{enumiii}} % i +\def\p@enumiii{\theenumi(\theenumii)} % 1(a)\it i) +\def\labelenumiv{\Alph{enumiv})} % A) +\def\theenumiv{\Alph{enumiv}} % A +\def\p@enumiv{\p@enumiii\theenumiii} % 1(a)\it i)A +\def\labelitemi{\m@th$-$} +\def\labelitemii{\m@th$\bullet$} +\def\labelitemiii{\m@th$\ast$} +\def\labelitemiv{{\footnotesize +}} +\def\descriptionlabel#1{\hspace\labelsep \bf #1} +\newenvironment{description}{% + \list{}{% + \labelwidth\z@ + \itemindent -\leftmargin + \let\makelabel\descriptionlabel + }}{\endlist} +\newskip\topsepm@th +\if@kaplist + \def\kapitemargs{% + \topsep \z@ \@plus 1pt + \partopsep \z@ \@plus 1pt + \itemsep \z@ \@plus \z@ + \parsep \z@ \@plus 1pt + \if@margspec \else \leftmargini \z@ \fi + \if@margspec \else \leftmarginii 1em \fi + \if@margspec \else \leftmarginiii 1em \fi + \if@margspec \else \leftmarginiv 1em \fi + \if@margspec + \leftmargin\csname leftmargin\romannumeral\@itemdepth\endcsname + \labelwidth\leftmargin + \advance\labelwidth-\labelsep + \fi + \rightmargin \z@ + \listparindent \z@ + \itemindent \z@ + } + \def\kapenumargs{% + \topsep \z@ \@plus 1pt + \partopsep \z@ \@plus 1pt + \itemsep \z@ \@plus \z@ + \parsep \z@ \@plus 1pt + \if@margspec \else \leftmargini \z@ \fi + \if@margspec \else \leftmarginii 1em \fi + \if@margspec \else \leftmarginiii 1em \fi + \if@margspec \else \leftmarginiv 1em \fi + \if@margspec + \leftmargin\csname leftmargin\romannumeral\@enumdepth\endcsname + \labelwidth\leftmargin + \advance\labelwidth-\labelsep + \fi + \rightmargin \z@ + \listparindent \z@ + \itemindent \z@ + } + \renewcommand{\@mklab}[1]{#1\hfil} % for custom list env-s only +\else +\def\kapenumargs{} +\def\kapitemargs{} +\fi +\def\@@enum@label#1{\hss \llap{#1}} % may stick out into l. margin +\def\@@item@label#1{\hss #1\hfil} +\def\enumerate{\@ifnextchar[% + {\kap@enumerate}% + {\if@margspec \kap@enumerate[] \else \kap@enumerate[00] \fi }} +\def\kap@enumerate[#1]{% + \ifnum \@enumdepth >3 \@toodeep\else + \advance\@enumdepth \@ne + \edef\@enumctr{enum\romannumeral\the\@enumdepth} + \list{\csname label\@enumctr\endcsname}{% + \topsepm@th \topsep + \kapenumargs + \usecounter{\@enumctr} + \settowidth\labelwidth{#1.} + \setlength{\@tempdima}{\labelwidth} + \addtolength{\@tempdima}{\labelsep} + \if@margspec + \ifdim \@tempdima > \leftmargin + \setlength{\leftmargin}{\@tempdima} + \fi + \else + \setlength{\leftmargin}{\@tempdima} + \fi + \let\makelabel\@@enum@label} + \fi + } +\let\endenumerate\endlist + +\def\itemize{\@ifnextchar[{\kap@itemize}{\kap@itemize[]}} +\def\kap@itemize[#1]{\def\klu@arg{#1}% + \ifnum \@itemdepth >3 \@toodeep + \else + \advance\@itemdepth \@ne + \edef\@itemitem{labelitem\romannumeral\the\@itemdepth}% + \ifx \klu@arg\empty + \list {\csname\@itemitem\endcsname}{% + \topsepm@th \topsep + \kapitemargs + \let\makelabel\@@item@label} + \else + \list {\klu@arg }{% + \kapitemargs + \let\makelabel\@@item@label + } + \fi + \fi + } +\let\enditemize\endlist +\def\verse{\let\\=\@centercr + \list{}{\itemsep\z@ + \itemindent -1.5em + \listparindent \itemindent + \rightmargin\leftmargin + \advance\leftmargin 1.5em + }\item[]} +\let\endverse\endlist + +\def\quotation{\quoteskip + \list{}{% + \listparindent 1.5em + \topsep .5ex plus 2pt minus 1pt + \itemindent\listparindent + \parsep 0pt plus 1pt + }\item[] + \hskip-\listparindent} +\def\endquotation{\endlist\quoteskip} + +\def\quote{\quoteskip\list{}{% + \leftmargin 1.5em + \topsep .5ex plus 2pt minus 1pt + }\item[]} +\def\endquote{\endlist\quoteskip} +\def\quoteskip{} + +\def\frontmatter{\begingroup\thispagestyle{empty}% + \renewcommand{\thepage}{\roman{page}}\setcounter{page}{1}} +\def\endfrontmatter{\newpage\endgroup\setcounter{page}{1}} +\newenvironment{notes}{\sectioncmd*{\notesname}\footnotesize + \begin{enumerate}}{\end{enumerate}% + \par \vskip 6pt \@plus 12pt \@minus 2pt} +\def\notesname{Notes} +\newenvironment{vitae}{% + \begingroup + \setcounter{enumiv}{0}% + \global\setbox0=\vbox\bgroup + }{% + \egroup + \ifnum \c@enumiv > 1 + \par\section*{\multiplevitaename}% + \else + \par\section*{\vitaename}% + \fi + \unvbox0 \endgroup \par + \vspace{24pt}% + } +\newcommand{\Vauthor}[1]{% + \addtocounter{enumiv}{1}% + \subsubsection*{#1}% + } + \def\vitaename{Author's Vitae}% + \def\multiplevitaename{Authors' Vitae}% +\newbox\aobox +\newenvironment{ao}{% + \global\setbox\aobox + \vbox\bgroup + \footnotesize\noindent + \ifx\offprintsaddress\empty + \leavevmode + \else + {\it \offprintsaddress:\/}\ + \fi + } + {\par\vskip18pt\egroup} +\newcommand{\make@ao}{% + \@tempdima \ht\aobox + \ifdim \@tempdima > 0pt + \vskip 1pc % added by SK + \par\noindent \unvbox\aobox + \fi + } +\newcommand{\offprintsaddress}{Address for Offprints} +\newenvironment{thenomenclature}{\section*{Nomenclature} + \parbox[t]{.48\textwidth}\bgroup\parindent 0pt + \footnotesize \begin{tabular}{p{2pc}p{11pc}}}{% + \end{tabular}\egroup} +\newcommand{\splitnomen}{\end{tabular}\egroup~\parbox[t]{.48\textwidth}% + \bgroup\parindent 0pt \footnotesize \begin{tabular}{p{2pc}p{11pc}}} +\newcommand{\nmc}[1]{\parbox[t]{11pc}{\raggedright #1}} +\def\verbatim@font{\normalsize\tt} +\def\acknowledgementsname{Acknowledgements}% +\def\acknowledgements{\section*{\acknowledgementsname}% + \message{\acknowledgementsname}} +\def\endacknowledgements{\par \bigskip} +\gdef\title#1{\title@{#1}} +\gdef\author#1{\author@{#1}} +\gdef\date#1{\date@{#1}} +\gdef\nodagger@{% + \def\@fnsymbol##1{\ensuremath{\ifcase##1\or *\or \ddagger\or + \mathsection\or \mathparagraph\or \|\or ** + \or \ddagger\ddagger \else\@ctrerr\fi}}} +\def\opening{% + \let\title=\title@ + \let\author=\author@ + \let\date=\date@ + \let\arttype=\arttype@ + \let\subtitle=\subtitle@ + \let\dedication=\dedication@ + \let\translation=\translation@ + \let\received=\received@ + \let\orf=\orf@ + \let\accepted=\accepted@ + \let\revised=\revised@ + \let\institute=\institute@ + \hsize\textwidth + \let\nodagger\nodagger@ + } +\gdef\maketitle{\endopening} +\def\endopening{% + \ifx\listfiles\@notprerr \maketitle@@ \else + \AtBeginDocument{\maketitle@@}\fi + \gdef\title##1{\opening@only\title} + \gdef\subtitle##1{\opening@only\subtitle} + \gdef\orf##1{\opening@only\orf} + \gdef\dedication##1{\opening@only\dedication} + \gdef\translation##1{\opening@only\translation} + \gdef\received##1{\opening@only\received} + \gdef\revised##1{\opening@only\revised} + \gdef\author##1{\opening@only\author} + \gdef\institute##1{\opening@only\institute} + \gdef\date##1{\opening@only\date}% + \gdef\arttype##1{\opening@only\arttype} + \gdef\nodagger{\opening@only\nodagger} + } +\def\opening@only#1{\PackageWarning{kluopen}{\string#1\space + effective only inside opening environment.}} +\def\authorsize{\normalsize \raggedright} +\def\authorcase#1{#1} +\def\authorindent{0pt} +\def\afterallauthorsskip{1em\relax} +\def\afterauthorskip{0pt} +\def\institutesize{\footnotesize\it} +\def\institutecase#1{#1} +\def\instituteindent{0pt} +\def\institutesep{.4\baselineskip} +\def\authorand{and} +\def\i@oldseries{} +\newtoks\@temptokenb +\long\def\append@item#1\to#2{% + \@temptokena={\@k@p{#1}}% + \@temptokenb=\expandafter{#2}% + \xdef#2{\the\@temptokenb\the\@temptokena}} +\def\get@left#1\to#2{\expandafter\g@l#1\g@l#1#2} +\long\def\g@l\@k@p#1#2\g@l#3#4{\def#4{#1}\def#3{#2}} +\def\@authors{}% +\def\@allauthors{}% +\def\@institutes{}% +\def\@instituteauthors{}% +\def\@curauths{} +\def\@curinst{} +\def\author@#1{\append@item#1\to\@authors + \append@item#1\to\@allauthors } +\def\institute@#1{\append@item#1\to\@institutes + \expandafter\append@item\expandafter{\@authors}\to\@instituteauthors + \gdef\@authors{}} +\newif\ifthanks +\def\orf@#1{#1} +\def\@formatname#1#2{\begingroup + \def\thanks##1{\global\thankstrue}\setbox0\vbox{#1}% + \endgroup + \begingroup + \ifthanks + \edef\fn##1\thanks##2{\authorcase{##1}\/% + \noexpand\thanks{##2}#2}\expandafter\fn#1 + \else + \edef\fn##1{{\authorcase{##1}}#2}% + \expandafter\fn\expandafter{#1}% + \fi + \endgroup\global\thanksfalse } +\newcount\cnt@authors +\def\@formatauthors{\begingroup + \authorsize + \leavevmode + \gdef\surname##1{##1}% + \gdef\email##1{ \hbox{({\tt \lowercase{##1}})}}% + \cnt@authors=0 + \def\@k@p##1{\advance\cnt@authors by 1}\@curauths + \def\@k@p##1{\advance\cnt@authors by -1 + \ifnum\cnt@authors>1 + \@formatname{##1}{,}\penalty0\ \fi % signif. space + \ifnum\cnt@authors=1 % before \fi's !! + \@formatname{##1}{} \authorand \penalty0\ \fi + \ifnum\cnt@authors<1 + \@formatname{##1}{}\par\fi}\@curauths + \vskip \afterauthorskip + \endgroup} +\def\@formatinstitute{{\institutesize \institutecase{\@curinst}\par}} +\newcount\cnt@institutes +\def\@authorsandinstitutes{\begingroup + \authorsize + \cnt@authors=0 + \def\@k@p##1{\advance\cnt@authors by 1}\@allauthors + \cnt@institutes=0 + \def\@k@p##1{\advance\cnt@institutes by 1}\@institutes\relax + \ifnum\cnt@institutes=0 + \let\@curauths\@allauthors + \parindent=\authorindent + \hangindent=\authorindent + \@formatauthors + \fi + \loop\ifnum\cnt@institutes>0 + \get@left\@instituteauthors\to\@curauths + \parindent=\authorindent + \hangindent=\authorindent + \@formatauthors + \get@left\@institutes\to\@curinst + \parindent=\instituteindent + \hangindent=\instituteindent + \@formatinstitute + \ifnum\cnt@institutes>1 \vskip \institutesep\relax \fi + \advance\cnt@institutes by -1 + \repeat + \vskip \afterallauthorsskip + \gdef\@authors{}% + \gdef\@allauthors{}% + \gdef\@institutes{}% + \gdef\@instituteauthors{}% + \gdef\@curauths{}% + \gdef\@curinst{}% +\endgroup} +\def\titleflushstyle{} +\def\titlefont{\Large\rm} +\def\titlecase#1{#1} +\def\titleindent{0pt} +\def\aftertitleskip{1.8pc } +\def\presubtitleskip{-1.4pc } +\def\aftersubtitleskip{1pc } +\def\subtitlefont{\large\it} +\def\subtitleflushstyle{} +\def\title@#1{\gdef\@title{% + \@formattitle{#1}\par \vskip \aftertitleskip }} +\def\@title{} +\def\@formattitle#1{\begingroup + \def\thanks##1{\global\thankstrue}% + \setbox\@tempboxa\vbox{#1}\endgroup + \begingroup + \titleflushstyle + \ifthanks + \def\fn##1\thanks##2{\ititle@{##1}{\,\thanks{##2}}}% + \expandafter\fn#1 + \else + \def\fn##1{\ititle@{##1}{}}\expandafter\fn\expandafter{#1}% + \fi + \endgroup\global\thanksfalse } +\def\titlebaselinefactor{1.05} +\def\ititle@#1#2{\begingroup + \parindent \titleindent + \hangindent \titleindent + \hyphenpenalty10000 + {\titlefont\titlecase{#1}#2% + \baselineskip=\titlebaselinefactor\baselineskip + \par} + \endgroup} +\def\@subtitle{} +\def\subtitle@#1{\gdef\@subtitle{\vskip \presubtitleskip + \@formatsubtitle{#1}\par \vskip \aftersubtitleskip }} +\def\@formatsubtitle#1{\begingroup + \def\thanks##1{\global\thankstrue}\setbox0\vbox{#1}\endgroup + \begingroup \subtitleflushstyle + \ifthanks + \def\fn##1\thanks##2{\subtitle@thanks{##1}{##2}}\expandafter\fn#1 + \else + \def\fn##1{\subtitle@@{##1}}\expandafter\fn\expandafter{#1}\fi + \endgroup + \par\global\thanksfalse} +\def\subtitle@thanks#1#2{\isubtitle@{#1}\thanks{#2}\par + \ignorespaces} +\def\subtitle@@#1{\isubtitle@{#1}\par\ignorespaces} +\def\isubtitle@#1{{\subtitlefont #1}} +\def\afterdateskip{.7\baselineskip} +\def\datesize{\footnotesize} +\def\@date{{\i@oldseries\datesize Received: \@received ; + Accepted\@accepted}\vskip \afterdateskip + \gdef\@received{\ldots\ldots}% + \gdef\@accepted{\ldots\ldots}} +\def\date@#1{\gdef\@date{{\i@oldseries\datesize #1\par}\vskip \afterdateskip + \gdef\@received{\ldots\ldots}% + \gdef\@accepted{\ldots\ldots}}} +\def\@received{\ldots\ldots} +\def\@accepted{: \ldots\ldots} +\def\revised@#1{\gdef\@accepted{ in revised form: #1}} +\def\received@#1{\gdef\@received{#1}} +\def\accepted@#1{\gdef\@accepted{ in final form: #1}} +\def\artsize{\normalsize\it} +\def\afterartskip{1.5pc} +\def\beforeartskip{0pc} +\def\@arttype{} +\def\arttype@#1{\gdef\@arttype{\vskip\beforeartskip\noindent + {\artsize #1\vskip\afterartskip}}} +\def\@dedication{} +\def\dedicationsize{\normalsize\it\raggedright} +\def\prededicationskip{18pt} +\def\afterdedicationskip{18pt} +\def\dedication@#1{\gdef\@dedication{% + \unskip\vskip \prededicationskip + {\dedicationsize #1\par}% + \vskip \afterdedicationskip}} +\def\@translation{} +\def\translationsize{\normalsize\it\raggedright} +\def\pretranslationskip{18pt} +\def\aftertranslationskip{18pt} +\def\translation@#1{\gdef\@translation{% + \unskip\vskip \pretranslationskip + {\translationsize #1\par}% + \vskip \aftertranslationskip}} +\providecommand{\abstractname}{Abstract} +\providecommand{\keywordsname}{Keywords} +\providecommand{\abbreviationsname}{Abbreviations} +\providecommand{\nomenclaturename}{Nomenclature} +\def\abstractsize{\footnotesize} +\def\abstractnamefont{\bf} +\def\abstractdot{.~} +\def\keynamefont{\bf} +\def\nomennamefont{\bf} +\def\abbrevnamefont{\bf} +\def\classnamefont{\bf} +\def\afterabstractskip{.7\baselineskip\relax} +\def\preabstractskip{0pt\relax} +\newbox\@abstractbox +\def\@abstract{} +\newenvironment{abstract}{% + \gdef\@abstract{\message{\abstractname}% + {\vskip\preabstractskip + \noindent + \unvbox\@abstractbox + \vskip\afterabstractskip }}% + \global\setbox\@abstractbox\vbox\bgroup \abstractsize \noindent + {\abstractnamefont\abstractname\abstractdot}}{\par\egroup } +\def\@keywords{} +\long\def\keywords#1{% + \gdef\@keywords{\message{\keywordsname}% + {\abstractsize\noindent{\keynamefont + \keywordsname:~}#1\par \vskip.7\baselineskip}}} +\def\@abbreviations{} +\def\abbrev#1#2{#1 -- #2} +\long\def\abbreviations#1{% + \gdef\@abbreviations{\message{\abbreviationsname}% + {\abstractsize\noindent{\abbrevnamefont \abbreviationsname:~}% + #1\par \vskip.7\baselineskip}}} +\def\@nomenclature{} +\def\nomen#1#2{#1 -- #2} +\long\def\nomenclature#1{% + \gdef\@nomenclature{\message{\nomenclaturename}% + {\abstractsize\noindent{\nomennamefont + \nomenclaturename:\par}\noindent #1\par \vskip.7\baselineskip}}} +\def\@classification{} +\long\def\classification#1#2{% + \gdef\@classification{\message{Classification}% + {\abstractsize\noindent{\classnamefont #1: }% + #2\par \vskip.7\baselineskip}}} +\def\motto{\@ifnextchar[{\prosemotto}{\poemmotto}} +\newbox\mottobox +\def\@motto{} +\long\def\poemmotto{\global\setbox\mottobox\vbox \bgroup + \noindent + \hbox to\hsize\bgroup\begingroup + \hfill\vbox\bgroup\hsize =15pc + \footnotesize \raggedright \noindent + \parskip=3pt} +\long\def\prosemotto[#1]{\global\setbox\mottobox\vbox \bgroup + \noindent + \hbox to\hsize\bgroup \begingroup + \hfill\vbox\bgroup\hsize =15pc + \raggedright \footnotesize \noindent + \parskip=3pt} +\def\endmotto{\par \egroup \endgroup \egroup + \vspace{1\baselineskip}\egroup + \gdef\@motto{\par\message{Motto}\box\mottobox \gdef\@motto{}}} +\def\@maketitle{% + \@arttype \@title \@subtitle \@authorsandinstitutes \@date + \@abstract \@keywords \@abbreviations \@classification + \@nomenclature \@translation \@dedication \@motto} +\def\openingflushstyle{} +\def\maketitle@@{% + \begingroup + \setcounter{footnote}{0}% + \def\thefootnote{\fnsymbol{footnote}}% + \if@twocolumn + \twocolumn[{\openingflushstyle + \parindent 0pt + \@maketitle}] + \thispagestyle{opening}% + \@extramaketitle + \else + \newpage\global\@topnum\z@ + \thispagestyle{opening}% + {\openingflushstyle \parindent 0pt \@maketitle}% + \fi + \markboth{\@runningauthor}{\@runningtitle}% + \@thanks + \endgroup + \setcounter{footnote}{0}% + \let\@maketitle\relax + \gdef\@thanks{}% + \gdef\@title{}% + \let\thanks\relax } +\def\runningtitle#1{\gdef\@runningtitle{#1}} +\gdef\@runningtitle{} +\def\runningauthor#1{\gdef\@runningauthor{#1}} +\gdef\@runningauthor{} +\long\def\journaldata#1#2\dataend{% + \edef\@tempa{@#1}\ifx \@tempa\@currjournal #2\fi} +\def\CLsize{\footnotesize} +\def\@journal{} +\def\@currjournal{} +\def\journalcode#1{% + \edef\@currjournal{@#1}% + } +\def\i@oldseries{} +\newif\if@speccright \@speccrightfalse +\AtBeginDocument{\gdef\@speccrightcheck{% + \if@speccright + \footnotetext[4]{\@spectextone{} \@speccright{} \@spectexttwo}% + \fi }} +\def\@spectextone{The} +\newcommand\spectextone[1]{\gdef\@spectextone{#1}} +\def\@spectexttwo{right to retain a non-exclusive, royalty free + licence in and to any copyright is acknowledged.} +\newcommand\spectexttwo[1]{\gdef\@spectexttwo{#1}} +\newcommand\copyrightowner{\@ifstar{\crightA}{\crightB}} +\newcommand\crightA[1]{\gdef\@speccright{#1}\global\@speccrighttrue} +\newcommand\crightB[1]{\gdef\@copyrightowner{#1}\global\@speccrightfalse} +\def\@speccright{} +\def\@copyrightowner{Kluwer Academic Publishers} +\newcommand\country[1]{\gdef\@country{#1}} +\def\@country{the Netherlands} +\newcommand\volume[1]{\gdef\@volume{#1}} +\def\@volume{00} +\newcommand\pubyear[1]{\gdef\@pubyear{#1}} +\def\@pubyear{\number\year} +\newif\iflastpagegiven \lastpagegivenfalse +\newcommand\firstpage[1]{% + \gdef\@firstpage{#1}% + \ifnum\@firstpage>\c@page + \setcounter{page}{#1}% + \PackageWarning{kluopen}{Increasing pagenumber to \@firstpage}% + \else \ifnum\@firstpage<\c@page + \PackageWarning{kluopen}{Firstpage lower than pagenumber}\fi\fi + \xdef\@firstpage{\the\c@page}% + } +\def\@firstpage{1} +\def\pagenumbering#1{% + \global\c@page \@ne + \gdef\thepage{\csname @#1\endcsname \c@page}% + \gdef\thefirstpage{% + \csname @#1\endcsname \@firstpage}% + \gdef\thelastpage{% + \csname @#1\endcsname \@lastpage}% + } +\pagenumbering{arabic} +\newcommand\lastpage[1]{\xdef\@lastpage{#1}% + \global\lastpagegiventrue} +\def\@lastpage{0} +\def\setlastpage{\iflastpagegiven\else + \edef\@tempa{@lastpage@\the\c@article}% + \expandafter + \ifx \csname \@tempa \endcsname \relax + \gdef\@lastpage{0}% + \else + \xdef\@lastpage{\@nameuse{@lastpage@\the\c@article}}% + \fi + \fi } +\def\writelastpage{% + \iflastpagegiven \else + \immediate\write\@auxout% + {\string\global\string\@namedef{@lastpage@\the\c@article}{\the\c@page}}% + \fi + } +\def\thepagerange{% + \ifnum\@lastpage =0 {\ \bf PLEASE RUN AGAIN} \else + \ifnum\@lastpage = \@firstpage \ \thefirstpage\else + \ \thefirstpage--\thelastpage \fi\fi} +\def\@prin{Printed in} +\@ifundefined{textcopyright}{\def\textcopyright{\copyright}}{} +\def\copyrightline{\textcopyright~\i@oldseries\@pubyear\ + {\it\@copyrightowner.~~\@prin\ \@country.}\hfill\hbox{}} +\def\volsep{: } +\def\thejournal{\ifx\@journal\empty\else\leavevmode \i@oldseries + {\it\@journal\/}~~{\bf\i@oldseries\@volume\volsep}\thepagerange, + \@pubyear.\hfill\hbox{}\\ \fi} +\def\no{no} +\def\crline#1{\gdef\@crline{#1}} +\def\thecopyright{\ifx\@crline\no \else \copyrightline \par \fi } +\newtoks\logotoks +\catcode`\%=12 +\catcode`\#=12 +\logotoks={\special{" +4 4 translate +989 1138 1 [60 0 0 -60 210 930] +currentfile +/ASCII85Decode filter +<< /K -1 /Columns 989 >> +/CCITTFaxDecode filter +image +Q>'H49/K0rjdMhW-(A!cb;A.`/DC9EH"NLrmTGB3G`p9Q"2Q+cbR4Nj7'd7dn1Os5 +\string$DPm^#D5dp.Sq0)HOI.%W!@rm_0-3j?%po`_0-3j?%VDq_0-W'Fr+S1(LXi_Ye(:I +]*kjT\string$a@6KL"blG_X2L_CTtEVL"blG_X2L_CTtEVY/9RL]*l%#ln6muG.V%6g?j&" +CUMm`Fr+r%g?j'q?%q#"G.V%_f3rj7?*;dp[G("lm<6*IY1IHshmM2*G.V%_f7)=e +[G("lm<6*Iqd\string$AVIb/AMCUMmbg?j'qp:FV5rN=b\string$f7)=e^MCT"[GSCL[G(*'m<@rA +m<6,8\string\:3%Yf7)>#f7)>#f7)>#f7)>#f7)>#f7)>#f7)>#f7)>#rN?+r?2Iq)p:L(d +GOO8ShmM@LhnNsAIb0&IY5S7k]D(dJn)(P1^OFd`rVKmtp:L(fg@*q6CVP>sqd'*n +n)(lq^OH.Yp[*1nhnOWlIf90<n(R6f^OH.Yp[@"SCVP>sqtKR:^OH.Yp[@"SCVP>s +qtKQ8s8U1@C);u92\string$r0TIf90<e+`=g^OH.YpZ,==\string\+]gYg\string\ZD'qgWPOrP,i8rnlK- +IrF`IDsdM<\string\+]gY<rV"2qgWPOol'6r^UNq9hcBa6g\string\ZJ=mIbDbrP,i8qR?1thqRGR +g\string\ZJ=X+,'TrP#E4^UNq5\string\+]gYgZYS:s0qsA>CC\string\p\string\,F'GI<PY"lYir`pAJk\string$g]\string$*4 +^:SmLos`Okqg[AbD?"OWhlXZ\string\p"T/KrP"TTpAJk\string$g]\string$*4^:Sj&s0pTuf&'cJ>CC\string\n +D=uZ_hb.nbI4`5\string$oX=e/f5K6t?,'TlG5Z:Ng\string\&&-Dq<fO^KZ,0qHJI(l#\string$H=V75&p +f&'cIQJ_E4>CYDlD=uZV\string\(>QLhd*s^hlchCoX=e/dbFH(f5ILprP"TT?+uW^XhMDq +/\string\\iG[ea3VG5>El[ea3VG5>El[ea3VG5>El[efC`[ea3V/\string\\iF/\string\[P.XhMDq/\string\[P. +95gZ9f5ILpdbF#'oX=U#J(s4)oX=U#I4`1!hb.mjhb.ma\string\'j\string$qD=k:5>CA*;QJW!c +oX=U#I4`1FI4`1!hb.ma\string\'j\string$qD=EkK95gZ9_HVF?^(T2bD=eV\string$$#T=CqHJ=n\string\'j\string$i +/\string\[P.95fJ!hb.m@[eNL6V74;LDl'q[>C7R%qHJ=i[eNL6V74;LDl'q[\string$ZC^,qHJ=Y +>C7a+_@(:8[eN.*n:KEQQJVs"^(T2Z"h2?QHm#lm6#H*aDh8@8Jm3UF[eLuRp`R\string$? +6#H*WD=C2:KGNGN/\string\XRt27@;0aCL\string$khf"Uu#*%Ks"Le+7OAWdIj>'(dl*n`EL,P%* +&6jO::U(jdL-R<W?Jcof\string$<nG'j>\string$a;@XEKW5W@E:h]\string\'fZTZ&2IlgdAO<XZ3Ig*T= +hna6h\string\+!b`J";.F81K*N-5drJr9P82JLC&riK=?dcL_O,/H-%Tm_N_SP<`=[r2g%Q +1&S&'fJid;r.0IP.XrTBC_ZpLs8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-! +s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-! +s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!s8W-!r-X"n +rVQ?XhnG_tIf90<n)(m/rVQ?XhnG_tIf90<n)(m/rUg'cp[@!8hnOX=o_n[]n)\string$pu +^OH.RrVQ?XhbW.EIenNlqs""Pn#,X3^7W/hqL8D?l215DVsiNWT>,jOIenNlo_n[O +qs""Pe+_>cn#,WPn)\string$pu^7W-3^O8=p5CGbE5CGbE5CGbE5CGcgrUg'\string\rUg'\string\qL89h +5CG_f^7S3Y:Z"sGn#+Y/e*6boo_nFYI6W-DT22BRVpjo-l1Fh#5CG_f:T*ZZe*6N\string$ +I6O9!Vpjo&qL(Q":T)\string\+o_Nu"T21.:I6O9!K_g*\string\T21.:I6O9!K_g*\string\'C#/a:T)'X +5+`/RpeRg)I6O80o_;48peQS>HmcdY-e%\string$<'B)+gl0qK%pa<q+-c%t[i1C>FT*b&n +L=7gF:P*s-i1C/I-c%t[j:;B)"QU(.PuEc.AeiBCZN4SP=c/;D"]f?=L:]C?)O[;? +Ai"3B!'gY\string~> +}} +\catcode`\%=14 +\catcode`\#=6 +\def\kaplogo{\advance\textwidth -2pc + \leavevmode\lower 8pt + \hbox to 24pt{\the\logotoks\hss}} +\if@copyrighthead + \gdef\@copyrighthead{{\parindent 0pt\vbox to\headheight {% + \hsize\textwidth \vss \kaplogo + \parbox{\textwidth}{\CLsize\thejournal\thecopyright}}}} + \gdef\@copyrightfoot{} +\else + \gdef\@copyrightfoot{{\parindent 0pt\rlap{\vbox to 0pt{% + \hsize\textwidth \vss \kaplogo + \parbox{\textwidth}{\CLsize\thejournal\thecopyright}\vss}}}} + \gdef\@copyrighthead{} +\fi +\def\@kapidenthead{} +\def\@kapidentfoot{} +\if@kapidenthead + \def\editor#1{\gdef\@kapidentfoot{}% + \if@noid \gdef\@kapidenthead{}\else + \gdef\@kapidenthead{\footnotesize \tt #1 (\klujnlname:\kluclassname)\ v.% + \kluclassversion\hfill}\fi} +\else + \def\editor#1{\gdef\@kapidenthead{}% + \if@noid \gdef\@kapidentfoot{}\else + \gdef\@kapidentfoot{\vbox to 0pt{% + \rlap{\vbox to \id@boxheight{\hbox{}\vfill + \hbox to \textwidth{\footnotesize\tt\hbox{}\hfill #1 + (\klujnlname:\kluclassname)\ v.\kluclassversion}% + \vskip 10pt}}\vss}}\fi} +\fi +\newcounter{outputpage} +\def\idline{\if@noid\else + \stepcounter{outputpage}% + \rlap{\smash{\vtop to \id@boxheight{% + \vfil\hbox to\textwidth{% + \hfil\footnotesize\tt + \jobname.tex; \TODAY;~\timenow;~p.\theoutputpage}}}}% + \fi} +\DeclareTextAccent{\@acci}{OT1}{19} +\DeclareTextAccent{\@accii}{OT1}{18} +\DeclareTextAccent{\@acciii}{OT1}{22} +\DeclareTextAccent{\@acci}{T1}{1} +\DeclareTextAccent{\@accii}{T1}{0} +\DeclareTextAccent{\@acciii}{T1}{9} +\gdef\markboth#1#2{{\let\protect=\noexpand + \xdef\myleftmark{\Uppercase{#1}}% + \xdef\myrightmark{\Uppercase{#2}}}} +\let\imarkboth\markboth +\def\myleftmark{} +\def\myrightmark{} +\def\@markfont{\rm\scriptsize} +\def\@pgnumfont{\rm\normalsize} +\def\ps@headings{% + \def\@oddfoot{\idline\hfil }% + \let\@evenfoot\@oddfoot + \def\@evenhead{\hbox{}\@pgnumfont\rlap{\thepage}\hfil + \@markfont\myleftmark\hfil}% + \def\@oddhead{\hbox{}\hfil\@markfont\myrightmark\hfil + \@pgnumfont\llap{\thepage}}% + \let\@mkboth\@gobbletwo + \def\chaptermark##1{}% + \def\sectionmark##1{}% + \def\subsectionmark##1{}} +\def\ps@myheadings{% + \def\@oddfoot{\idline\hfil }% + \let\@evenfoot\@oddfoot + \def\@evenhead{\hbox{}\@pgnumfont\rlap{\thepage}\hfill + \@markfont\myleftmark}% + \def\@oddhead{\hbox{}\@markfont\myrightmark\hfill + \@pgnumfont\llap{\thepage}}% + \let\@mkboth\@gobbletwo + \def\chaptermark##1{}% + \def\sectionmark##1{}% + \def\subsectionmark##1{}} +\def\ps@empty{% + \def\@oddfoot{\idline\hfil }% + \let\@evenfoot\@oddfoot + \def\@evenhead{}% + \def\@oddhead{}% + \let\@mkboth\@gobbletwo + \def\chaptermark##1{}% + \def\sectionmark##1{}% + \def\subsectionmark##1{}} +\let\ps@title\ps@empty +\let\ps@part\ps@empty +\let\ps@chapter\ps@empty +\def\ps@monoheadings{% + \let\@mkboth\@gobbletwo + \def\@oddfoot{\idline\hfil}% + \let\@evenfoot\@oddfoot + \def\@evenhead{\hbox{}\rm\normalsize\hbox to 0pt{\thepage\hss}\hfil + \footnotesize\myleftmark\hfil}% + \def\@oddhead{\hbox{}\rm\footnotesize\hfil + \myrightmark\hfil + \rm\normalsize\hbox to 0pt{\hss\thepage}}% + \def\chaptermark##1{% + \if@mainmatter + \markboth{\@chapapp\ \NUMTOWORD{\c@chapter}}{\@runningtitle}% + \else + \markboth{\@chapapp\ \thechapter}{\@runningtitle}% + \fi } + \let\sectionmark\@gobble + } + \def\ps@monotitle{\let\@mkboth\@gobbletwo + \def\@oddhead{\hbox{}\rm\footnotesize\hfil + \myleftmark\hfil}% + \def\@oddfoot{\idline \@barcode\@kapidentfoot + \parbox{\textwidth}{\hfil\thepage\hfil\\ \@copyrightfoot}} + \let\@evenhead\@oddhead + \let\@evenfoot\@oddfoot + \let\chaptermark\@gobbletwo + \let\sectionmark\@gobble + \let\subsectionmark\@gobble + } + \def\ps@monochapter{\let\@mkboth\@gobbletwo + \def\@oddhead{\hbox{}\hfil\rm\footnotesize + \myleftmark\hfil}% + \def\@oddfoot{\idline\hfil\rm\normalsize\thepage\hfil}% + \let\@evenhead\@oddhead + \let\@evenfoot\@oddfoot + \let\chaptermark\@gobbletwo + \let\sectionmark\@gobble + \let\subsectionmark\@gobble + } + \def\ps@editheadings{\let\@mkboth\@gobbletwo + \def\@oddfoot{\idline\hfil}% + \def\@evenfoot{\idline\hfil}% + \def\@evenhead{\hbox{}\rm\normalsize\rlap{\thepage}\hfil + \footnotesize\myleftmark\hfil}% + \def\@oddhead{\hbox{}\rm\footnotesize\hfil\myrightmark\hfil + \rm\normalsize\hbox to 0pt{\hss\thepage}}% + \def\chaptermark##1{% + \markboth{\@runningauthor}{\@runningtitle}}% + \let\sectionmark\@gobble + } + \def\ps@edittitle{\let\@mkboth\@gobbletwo + \def\@oddhead{\hbox{}\rm\footnotesize\hfil + \myleftmark\hfil}% + \def\@oddfoot{\idline \@barcode\@kapidentfoot + \parbox{\textwidth}{\hfil\raise 6pt\hbox{\thepage}\hfil\\ \@copyrightfoot}} + \let\@evenhead\@oddhead + \let\@evenfoot\@oddfoot} +\def\theinheadpage{\thepage} +\def\ps@opening{% + \def\@oddhead{\@copyrighthead \@kapidenthead\hss + \if@copyrighthead \llap{\theinheadpage}\fi }% + \let\@evenhead\@oddhead + \def\@oddfoot{\@copyrightfoot \@barcode\idline\@kapidentfoot\hss} + \let\@evenfoot\@oddfoot} +\newcounter{article} +\renewcommand{\thearticle}{} +\let\ilabel=\label +\let\iref=\ref +\let\ipageref=\pageref +\let\art@intdefinecounter\@definecounter +\newif\ifinarticle % \inarticlefalse +\newenvironment{article}{% + \def\@definecounter##1{\art@intdefinecounter{##1}% + \@addtoreset{##1}{article}}% + \renewcommand{\thearticle}{\roman{article}}% + \refstepcounter{article}% + \message{Article \number\c@article}% + \gdef\@firstpage{\the\c@page}% + \@addtoreset{equation}{article}% + \ifx\sectioncmd\section + \@addtoreset{section}{article}% + \else + \@addtoreset{chapter}{article}% + \fi + \@addtoreset{endnote}{article}% + \@addtoreset{table}{article}% + \@addtoreset{figure}{article}% + \@addtoreset{algorithm}{article}% + \def\label##1{\ilabel{\thearticle ##1}}% + \def\ref##1{\iref{\thearticle ##1}}% + \def\pageref##1{\ipageref{\thearticle ##1}}% + \setlastpage + \global\inarticletrue + }{\make@ao + \writelastpage + \clearpage + \if@openright + \ifodd \c@page \else ~\thispagestyle{empty}\newpage \fi + \fi + \gdef\@dedication{}\gdef\@translation{}% + \gdef\@title{}\gdef\@subtitle{}% + \gdef\@arttype{}\gdef\@keywords{}\gdef\@classification{}% + \gdef\@nomenclature{}\gdef\@abbreviations{}\gdef\@abstract{}% + \gdef\@kapidenthead{}\gdef\@kapidentfoot{}% + \gdef\@barcode{}\gdef\@firstpage{\thepage}% + \gdef\@crline{}% + \global\lastpagegivenfalse + \global\inarticlefalse + } +\AtBeginDocument{\setlastpage} +\AtEndDocument{\ifnum \c@article=0 + \writelastpage + \clearpage\fi} +\font\barcodefont=cmr10 +\def\barcode#1{\global\font\barcodefont=barcodes + \gdef\@barcode{\rlap{\vbox to 0pt{% + \vbox to \id@boxheight{\hbox{}\vfill + {\barcodefont \hbox{#1}}}\vss}}}} +\def\@barcode{} +\def\PIPSID#1{} +\parskip 0pt +\hyphenpenalty 200 +\doublehyphendemerits 640000 % corresponds to badness 800 +\finalhyphendemerits 1000000 % corresponds to badness 1000 +\arraycolsep 6pt +\tabcolsep 6pt +\arrayrulewidth .4pt +\doublerulesep 2pt +\def\@rcline[#1-#2]{% + \noalign{% + \global\@cla #1\relax + \global\advance\@cla\m@ne + \ifnum\@cla >0 + \global\let\@tabklu@tmpa\@rclinea + \else + \global\let\@tabklu@tmpa\@rclineb + \fi + \global\@clb #2\relax + \global\advance\@clb-\@cla }% + \@tabklu@tmpa + \noalign{\vskip-\arrayrulewidth}% + }% +\def\@rclinea{% + \multispan\@cla&\multispan\@clb + \hbox to 3pt{\hfil }% + \unskip + \leaders\hrule \@height \arrayrulewidth\hfill + \cr}% +\def\@rclineb{% + \multispan\@clb + \hbox to 3pt{\hfil }% + \unskip + \leaders\hrule \@height \arrayrulewidth\hfill + \cr}% +\def\@lcline[#1-#2]{% + \noalign{% + \global\@cla #1\relax + \global\advance\@cla\m@ne + \ifnum\@cla >0 + \global\let\@tabklu@tmpa\@lclinea + \else + \global\let\@tabklu@tmpa\@lclineb + \fi + \global\@clb #2\relax + \global\advance\@clb-\@cla + }\@tabklu@tmpa + \noalign{\vskip-\arrayrulewidth}% +}% +\def\@lclinea{% + \multispan\@cla&\multispan\@clb + \unskip + \leaders\hrule \@height \arrayrulewidth\hfill + \hbox to 3pt{\hfil }\cr}% +\def\@lclineb{% + \multispan\@clb + \unskip + \leaders\hrule \@height \arrayrulewidth\hfill + \hbox to 3pt{\hfil }\cr}% +\def\@lrcline[#1-#2]{% + \noalign{% + \global\@cla #1\relax + \global\advance\@cla\m@ne + \ifnum\@cla>0 + \global \let\@tabklu@tmpa\@lrclinea + \else + \global \let\@tabklu@tmpa\@lrclineb + \fi + \global \@clb #2\relax + \global \advance\@clb-\@cla + }% + \@tabklu@tmpa + \noalign{\vskip -\arrayrulewidth}% + }% +\def\@lrclinea{% + \multispan\@cla&\multispan\@clb + \hbox to 3pt{\hfil }% + \unskip\leaders\hrule \@height \arrayrulewidth\hfill + \hbox to 3pt{\hfil }% + \cr}% +\def\@lrclineb{% + \multispan\@clb + \hbox to 3pt{\hfil }% + \unskip\leaders\hrule \@height \arrayrulewidth\hfill + \hbox to 3pt{\hfil }% + \cr}% +\newlength\stretchtabsep +\setlength\stretchtabsep{0pt plus 1fil} +\AtBeginDocument{% +\let\savehline\hline +\def\tabular{\begingroup + \def\hline{\noalign{\vskip3pt}\savehline\noalign{\vskip3pt}}% + \def\rcline##1{\@rcline[##1]}% + \def\lcline##1{\@lcline[##1]}% + \def\lrcline##1{\@lrcline[##1]}% + \let\rlcline=\lrcline + \setbox\strutbox\hbox{\vrule height.8\baselineskip + depth.4\baselineskip width\z@}% + \setbox0=\hbox\bgroup\def\@halignto{}\@tabular}% +\def\endtabular{\crcr\egroup\egroup $\egroup + \egroup \tabwidth{\wd0}\unhbox0 \endgroup}% +\let\klu@intarray\array +\let\klu@intendarray\endarray +\def\array{\begingroup \let\hline\savehline \klu@intarray } +\def\endarray{\klu@intendarray \endgroup} +\@ifundefined{newcolumntype}{% array.sty not loaded +\@namedef{tabular*}#1{% + \begingroup + \let\savehline\hline + \def\hline{\noalign{\vskip3pt}\savehline\noalign{\vskip3pt}}% + \def\rcline##1{\@rcline[##1]}% + \def\lcline##1{\@lcline[##1]}% + \def\lrcline##1{\@lrcline[##1]}% + \let\rlcline=\lrcline + \setbox\strutbox\hbox{\vrule height.8\baselineskip + depth.4\baselineskip width\z@}% + \setbox0=\hbox\bgroup\def\@halignto{to #1}% + \def\@tabacol{\edef\@preamble{\@preamble + \tabskip \stretchtabsep \hskip \tabcolsep}}\@tabular}% +}{% array.sty loaded: +\@namedef{tabular*}#1{% + \begingroup + \let\savehline\hline + \def\hline{\noalign{\vskip3pt}\savehline\noalign{\vskip3pt}}% + \def\rcline##1{\@rcline[##1]}% + \def\lcline##1{\@lcline[##1]}% + \def\lrcline##1{\@lrcline[##1]}% + \let\rlcline=\lrcline + \setbox\strutbox\hbox{\vrule height.8\baselineskip + depth.4\baselineskip width\z@}% + \setbox0=\hbox\bgroup + \gdef\@halignto{to #1}% + \@tabular}% +} % end array.sty loaded +\@namedef{endtabular*}{\endtabular} +\def\TABULAR{% + \let\savehline\hline %compatibility + \let\rcline\cline \let\lcline\cline + \let\lrcline\cline \let\rlcline\cline + \setbox0=\hbox\bgroup\def\@halignto{}\@tabular}% +\def\endTABULAR{\crcr\egroup\egroup $\egroup + \egroup \tabwidth{\wd0}\unhbox0 }% +\@namedef{TABULAR*}#1{% + \let\savehline\hline %compatibility + \let\rcline\cline \let\lcline\cline + \let\lrcline\cline \let\rlcline\cline + \setbox0=\hbox\bgroup\def\@halignto{to #1}\@tabular}% +\@namedef{endTABULAR*}{\endtabular}} % end of AtBeginDocument +\setcounter{topnumber}{2} +\setcounter{bottomnumber}{1} +\setcounter{totalnumber}{3} +\setcounter{dbltopnumber}{2} +\renewcommand{\topfraction}{.85} +\renewcommand{\textfraction}{.01} +\renewcommand{\bottomfraction}{.4} +\renewcommand{\floatpagefraction}{.84} +\renewcommand{\dblfloatpagefraction}{.84} +\renewcommand{\dbltopfraction}{.7} +\def\figtabdot{.} +\def\tablename{Table}% +\def\figurename{Figure}% +\def\algorithmname{Algorithm}% +\newdimen\maxfloatwidth +\newbox\figtabbox +\newdimen\floatindent +\newdimen\@tabskip +\gdef\cap@type{0} +\newdimen\captionskip +\setlength\captionskip{6pt} +\newdimen\@tabwidth +\setlength\@tabwidth{\textwidth} +\def\tabwidth#1{\global\setlength\@tabwidth{#1}} +\def\@getmaxwidth{\maxfloatwidth=\hsize + \if@kaprotate \maxfloatwidth=\textheight \fi } +\def\@floatcorrect{\if@kaprotate\else + \advance\maxfloatwidth -\floatindent \fi } +\def\hbox@to@floatwidth#1{\leavevmode + \hbox to \@tabwidth{#1}} +\def\@getindent{% + \ifnum\cap@type=2 \else + \@tabwidth=\if@kaprotate \textheight \else \hsize \fi + \if@figindent\advance \@tabwidth -\floatindent \fi\fi + \ifnum\cap@type=1 + \if@figindent \@tabskip\floatindent + \else \@centeredfloat \fi + \else \ifnum\cap@type=2 + \if@tabindent \@tabskip\floatindent + \else \@centeredfloat \fi + \ifdim \@tabwidth > \maxfloatwidth + \@tabskip 0pt + \floatindent 0pt + \fi + \else + \@centeredfloat + \fi + \fi +} +\def\@centeredfloat{% + \floatindent\maxfloatwidth + \advance\floatindent by -\@tabwidth + \divide\floatindent by 2 + \@tabskip\floatindent + \if@kaprotate + \@tabskip\hsize + \advance\@tabskip by -\ht\figtabbox + \advance\@tabskip by -\dp\figtabbox + \divide\@tabskip by 2 + \fi +} +\newif\if@centeredfigcaption +\newif\if@centeredtabcaption +\@centeredtabcaptiontrue +\@centeredfigcaptiontrue +\def\indentedtabcaptions{\global\@centeredtabcaptionfalse } +\def\indentedfigcaptions{\global\@centeredfigcaptionfalse } +\def\indentedcaptions{\global\@centeredtabcaptionfalse + \global\@centeredfigcaptionfalse} +\newdimen\captionindent +\setlength\captionindent{0pt} +\newtoks\@floatcaption +\def\tabcapspace{.5em} +\def\tabcapfont{\footnotesize } +\long\def\@maketabcaption#1#2{\global\@floatcaption={#2}% + \message{\tablename\space\thetable \if@kaprotate + \space(rotated) \fi}} +\def\@klu@caption{% + \setbox1=\hbox{\tabcapfont\fnum@table\hskip\tabcapspace + \the\@floatcaption}% + \noindent + \ifdim\wd1 >\@tabwidth + {\if@centeredtabcaption\centering\else \hskip \captionindent\fi + \parbox[b]{\@tabwidth}{\tabcapfont\unhbox1}}% + \else + \hbox to \@tabwidth{% + \if@centeredtabcaption \hfil \else \hskip \captionindent\fi + \tabcapfont\fnum@table + \hskip\tabcapspace{\tabcapfont\the\@floatcaption}\hfil }% + \fi + \if@kaprotate \else \par \vskip -\baselineskip \fi + \par +} +\def\@klu@figcaption{% + \setbox1=\hbox{\figcapfont\fnum@figure\hskip\tabcapspace + \the\@floatcaption}% + \noindent + \ifdim\wd1 >\@tabwidth + {\if@centeredfigcaption\centering\else \hskip \captionindent\fi + \parbox{\@tabwidth}{\figcapfont\unhbox1}}% + \else + \hbox to \@tabwidth{% + \if@centeredfigcaption \hfil\else \hskip \captionindent\fi + \tabcapfont\fnum@figure + \hskip\tabcapspace{\figcapfont\the\@floatcaption}\hfil}% + \fi + \par +} +\def\splitcaptions{\splittabcaptions\splitfigcaptions} +\def\splittabcaptions{ + \def\@klu@caption{% + \setbox1=\hbox{\tabcapfont\the\@floatcaption}% + \noindent + \ifdim\wd1 >\@tabwidth + \hbox to \@tabwidth{\if@centeredtabcaption\hss\else + \hskip\captionindent\fi + \tabcapfont\fnum@table\hss}\vskip \tabcapspace + \vskip 6pt + {\if@centeredtabcaption\centering\fi + \hskip \captionindent + \parbox{\@tabwidth}{\tabcapfont\unhbox1}}% + \else + \hbox to \@tabwidth{% + \if@centeredtabcaption \hfil\else \hskip\captionindent\fi + \tabcapfont\fnum@table\strut\hfil }\vskip \tabcapspace + \hbox to \@tabwidth{% + \if@centeredtabcaption \hfil\else \hskip\captionindent \fi + \tabcapfont\the\@floatcaption \hfil }% + \if@kaprotate \else \par \vskip -\baselineskip \fi + \fi + \par +}} +\def\splitfigcaptions{\def\@klu@figcaption{% + \setbox1=\hbox{\figcapfont\the\@floatcaption}% + \noindent + \ifdim\wd1 >\@tabwidth + \hbox to \@tabwidth{\if@centeredfigcaption\hfil\else + \hskip\captionindent\fi + \figcapfont\fnum@figure\hfil}\vskip \tabcapspace + \vskip 6pt + {\if@centeredfigcaption\centering\fi \hskip \captionindent + \parbox{\@tabwidth}{\figcapfont\unhbox1}}% + \else + \hbox to \@tabwidth{% + \if@centeredfigcaption \hfil\else \hskip\captionindent\fi + \figcapfont\fnum@figure\strut\hfil }\vskip \tabcapspace + \hbox to \@tabwidth{% + \if@centeredfigcaption \hfil\else \hskip\captionindent\fi + \figcapfont\the\@floatcaption \hfil }% + \fi + \par +}}% +\@ifundefined{thetable}{\newcounter{table}}{} +\def\thetable{\arabic{table}} +\def\fps@table{tbp} +\def\ftype@table{2} +\def\ext@table{lot} +\def\fnum@table{\tablename~\thetable\figtabdot} +\newif\if@tabindent \@tabindentfalse +\def\tableindent#1{% + \global\floatindent= #1\global\@tabindenttrue } +\def\tabfont{\footnotesize} +\def\@tabnotes{} +\newcounter{tabnote} +\def\tabnotemark{\ensuremath{^{\thetabnote}}} +\def\thetabnote{\arabic{tabnote}} +\def\tabnotesep{\par} +\def\tabnote#1{\stepcounter{tabnote}% + \rlap{\tabnotemark }% + \begingroup + \let\tabnotesep\relax + \xdef\@tabnotes{\@tabnotes\tabnotesep \tabnotemark #1\par}% + \endgroup } +\long\def\tabnotes#1{\gdef\@tabnotes{{\tabfont\noindent #1\par}}} +\def\@setnotrotatedtabbox{% + \setbox4=\hbox to \maxfloatwidth{\vbox{\hsize=\maxfloatwidth + \@klu@caption + \vskip\captionskip \leavevmode + \unvbox\figtabbox\par + \noindent\parbox{\@tabwidth}{\tabfont\@tabnotes}\par}}% + \if@fixedfloat\calc@fixedspace4\fi + \noindent\kern \floatindent\box4 + } +\def\@setrotatedtabbox{\begingroup \hfuzz=\vsize + \setbox2\hbox to \textheight{\hfil + \vbox to \hsize{\hsize=\vsize + \vfil + \hbox{\hbox@to@floatwidth{\vbox{\@klu@caption }}} + \vskip\captionskip + \hbox{\hbox@to@floatwidth{\box\figtabbox\hss}}% + \hbox{\hbox@to@floatwidth{\parbox{\@tabwidth}{\tabfont\@tabnotes}\hfil }}% + \vss + }\hss}\rotl{2}\endgroup +} +\def\table{\let\@makecaption\@maketabcaption + \global\@floatcaption={}% + \gdef\@tabnotes{}\setcounter{tabnote}{0}\gdef\cap@type{2}% + \@ifnextchar[{\t@blewithoptions}{\t@blewithoptions[tbp]}} +\def\t@blewithoptions[#1]{% + \if H#1\@fixedtable \else \@float{table}[#1]\fi + \@getmaxwidth \if@tabindent \@floatcorrect \fi + \setbox\figtabbox\vbox\bgroup\tabfont + \if@kaprotate\hfuzz=\vsize\fi }% +\def\endtable{\egroup \@getindent + \gdef\cap@type{0}\noindent + \hfuzz=\floatindent + \if@kaprotate \@setrotatedtabbox + \else \@setnotrotatedtabbox \fi + \if@fixedfloat \vskip\intextsep \@fixedfloatfalse + \else \end@float \fi + \hfuzz =0.1pt }% +\@namedef{table*}{\let\@makecaption\@maketabcaption + \global\@floatcaption={}% + \gdef\@tabnotes{}\setcounter{tabnote}{0}\gdef\cap@type{2}% + \@ifnextchar[{\dt@blewithoptions}{\dt@blewithoptions[tbp]}} +\def\dt@blewithoptions[#1]{% + \if H#1\if@twocolumn \@dblfloat{table}[t]\else \@fixedtable\fi + \else \@dblfloat{table}[#1]\fi + \@getmaxwidth \if@tabindent \@floatcorrect \fi + \setbox\figtabbox\vbox\bgroup\tabfont + \if@kaprotate \hfuzz=\vsize \fi }% +\@namedef{endtable*}{\egroup \@getindent + \gdef\cap@type{0}\noindent + \hfuzz=\floatindent + \if@kaprotate \@setrotatedtabbox + \else \@setnotrotatedtabbox \fi + \if@fixedfloat \vskip\intextsep \@fixedfloatfalse + \else \end@dblfloat \fi + \hfuzz=0.1pt }% +\newif\if@fixedfloat +\def\@fixedtable{\vskip\intextsep \@fixedfloattrue + \def\caption{\@ifnextchar[{\f@xedcap{table}}% + {\f@xedcap{table}[]}}} +\def\@fixedfigure{\vskip\intextsep \@fixedfloattrue + \def\caption{\@ifnextchar[{\f@xedcap{figure}}% + {\f@xedcap{figure}[]}}} +\def\f@xedcap#1[#2]#3{\refstepcounter{#1}\def\@tempa{#2}% + \ifx\@tempa\empty + \else \addcontentsline{\csname ext@#1\endcsname}{#1}{#2}\fi + \message{#1\space\csname the#1\endcsname \space (fixed)}% + \global\@floatcaption={#3}} +\def\calc@fixedspace#1{% + \@tempdima=\pagegoal + \@tempdimb=\dp#1 + \advance\@tempdimb \ht#1 + \advance\@tempdima -\pagetotal + \advance\@tempdima -2\intextsep + \wlog{pageleft= \the\@tempdima, + size= \the\@tempdimb }% + \ifdim\@tempdima>\@tempdimb \else \newpage \fi} +\@ifundefined{thefigure}{\newcounter{figure}}{} +\def\thefigure{\arabic{figure}} +\def\fps@figure{tbp} +\def\ftype@figure{1} +\def\ext@figure{lof} +\def\fnum@figure{\figurename~\thefigure\figtabdot} +\newif\if@figindent \@figindentfalse +\def\figindent#1{% + \global\floatindent #1 + \global\@figindenttrue } +\def\figcapfont{\footnotesize} +\long\def\@makefigcaption#1#2{% + \message{\figurename\space\thefigure + \if@kaprotate \space (rotated)\fi }% + \global\@floatcaption={#2}} +\def\figure{% + \gdef\cap@type{1}% + \let\@makecaption\@makefigcaption + \global\@floatcaption={}% + \@ifnextchar[{\f@gurewithoptions}{\f@gurewithoptions[tbp]}}% +\def\f@gurewithoptions[#1]{% + \let\saved@centerline\centerline + \if H#1\@fixedfigure \else \@float{figure}[#1]\fi + \@getmaxwidth \if@figindent \@floatcorrect + \def\centerline##1{##1}\fi + \setbox\figtabbox\vbox\bgroup }% +\def\endfigure{\egroup + \@getindent \gdef\cap@type{0}% + \hfuzz=\floatindent + \if@kaprotate \@setrotatedfigbox \pagebreak + \else \@setnotrotatedfigbox \fi + \let\centerline\saved@centerline + \if@fixedfloat \vskip\intextsep \@fixedfloatfalse + \else \end@float \fi + \hfuzz=0.1pt }% +\@namedef{figure*}{% + \def\cap@type{1}% + \let\@makecaption\@makefigcaption + \global\@floatcaption={}% + \@ifnextchar[{\df@gurewithoptions}{\df@gurewithoptions[ttp]}} +\def\df@gurewithoptions[#1]{% + \let\saved@centerline\centerline + \if H#1 \@fixedfigure \else \@dblfloat{figure}[#1]\fi + \@getmaxwidth \if@figindent \@floatcorrect + \def\centerline##1{##1}\fi + \setbox\figtabbox\vbox\bgroup }% +\@namedef{endfigure*}{\egroup + \@getindent \gdef\cap@type{0}% + \hfuzz=\floatindent + \if@kaprotate \@setrotatedfigbox + \else \@setnotrotatedfigbox \fi + \let\centerline\saved@centerline + \if@fixedfloat \vskip\intextsep \@fixedfloatfalse + \else \end@dblfloat \fi + \hfuzz=0.1pt }% +\def\@setnotrotatedfigbox{% + \setbox4=\hbox to \maxfloatwidth{\vbox{\hsize=\maxfloatwidth + \unvbox\figtabbox + \vskip\captionskip + \@klu@figcaption }}% + \if@fixedfloat\calc@fixedspace4 \fi + \noindent\kern \floatindent\box4 +} +\def\@setrotatedfigbox{% + \setbox2\vbox to \hsize{\hsize=\textheight + \leavevmode + \vrule width \textheight height 0pt depth 0pt\par + \vskip \@tabskip + \hbox to \textheight{\hss\box\figtabbox\hss}% + \vskip\captionskip + \hbox to \textheight{\vbox{\@klu@figcaption }} + \vss + }\rotl{2}}% +\newcounter{algorithm} +\def\thealgorithm{\arabic{algorithm}} +\def\fps@algorithm{tbp} +\def\ftype@algorithm{4} +\def\ext@algorithm{lof} +\long\def\@makealgocaption#1#2{% + \hbox to \hsize{\parbox[t]{\hsize}{{\vskip 1ex \tabcapfont + #1\figtabdot~~#2}}}} +\def\fnum@algorithm{\algorithmname\space \thealgorithm} +\def\algorithm{\let\@makecaption\@makealgocaption + \@float{algorithm}\footnotesize\obeyspaces\obeylines} +\let\endalgorithm\end@float +\def\subtable{\@ifnextchar[{\@subtable}{\@subtable[alph]}} +\def\@subtable[#1]{\refstepcounter{table}% + \def\@testoption{arabic}\def\@testparam{#1}% + \begingroup + \edef\old@table{\the\c@table}% + \edef\old@thetable{\thetable}% + \setcounter{table}{0}% + \ifx\@testoption\@testparam + \def\thetable{\old@thetable.\csname #1\endcsname{table}}% + \else + \def\thetable{\old@thetable\csname #1\endcsname{table}}% + \fi} +\def\endsubtable{\setcounter{table}{\old@table}% + \endgroup \global\@ignoretrue} +\def\subfigure{\@ifnextchar[{\@subfigure}{\@subfigure[alph]}} +\def\@subfigure[#1]{\refstepcounter{figure}% + \def\@testoption{arabic}\def\@testparam{#1}% + \begingroup + \edef\old@figure{\the\c@figure}% + \edef\old@thefigure{\thefigure}% + \setcounter{figure}{0}% + \ifx\@testoption\@testparam + \def\thefigure{\old@thefigure.\csname #1\endcsname{figure}}% + \else + \def\thefigure{\old@thefigure\csname #1\endcsname{figure}}% + \fi} +\def\endsubfigure{\setcounter{figure}{\old@figure}% + \endgroup \global\@ignoretrue} + +\newif\if@kaprotate \@kaprotatefalse +\def\kaprotate{\global\@kaprotatetrue} +\def\endkaprotate{\global\@kaprotatefalse} + +\newdimen\rotdimen +\def\rotstart#1{\special{ps: gsave currentpoint currentpoint translate + #1 neg exch neg exch translate}} +\def\rotfinish{\special{ps: currentpoint grestore moveto}} +\def\rotl#1{\rotdimen=\ht#1\advance\rotdimen by \dp#1 + \hbox to \rotdimen{\vbox to\wd#1{\vskip \wd#1 + \rotstart{270 rotate}\box #1\vss}\hss}\rotfinish} +\def\rotr#1{\rotdimen=\ht #1\advance\rotdimen by \dp#1 + \hbox to \rotdimen{\vbox to \wd#1{\vskip \wd#1 + \rotstart{90 rotate}\box #1\vss}\hss}\rotfinish} +\def\footnoterule{\kern-3\p@ + \hrule width 3pc + \kern 2.6\p@} +\long\def\@makefntext#1{\parindent 1em\noindent + \hbox to 1.5em{\hss\textsuperscript{\@thefnmark}}% + \hskip0.5em\footnotesize#1} +\def\@makefnmark{\hbox{\textsuperscript{\@thefnmark}}} +\footnotesep 6pt +\skip\footins 10pt plus 4pt minus 2pt +\newcounter{endnote} +\def\theendnote{\arabic{endnote}} +\def\@makeenmark{\hbox{$^{\@theenmark}$}} +\newdimen\endnotesep +\setlength\endnotesep{1pt} +\def\notesname{Notes}% <------ JK +\def\endnotesize{\footnotesize} +\def\endnoteformat{\vskip\endnotesep + \rightskip\z@ \leftskip\z@ + \parindent=1.8em\leavevmode\llap{\hbox{$^{\@theenmark}$ }}} +\def\endnote{% + \@ifnextchar[ + {\@xendnote}% + {\stepcounter{endnote}% + \xdef\@theenmark{\theendnote}% + \@endnotemark + \@endnotetext}} +\long\def\addtoendnotes#1{% + \if@endnotesopen \else \@openendnotes \fi + \begingroup + \newlinechar='40 + \let\protect\string + \if@filesw \immediate\write\@endnotes{#1}\fi + \endgroup} +\def\theendnotes{% + \if@filesw \immediate\closeout\@endnotes \fi + \global\@endnotesopenfalse + \begingroup + \makeatletter + \def\@doanendnote##1##2>{% + \def\@theenmark{##1}% + \par\begingroup + \endnoteformat}% + \def\@endanendnote{\par\endgroup}% + \def\ETC.{\PackageError{klunote}{% + Some endnotes will be truncated}{% + Because of memory constraints, LaTeX truncated some\MessageBreak + long endnotes while writing the auxiliary file.\MessageBreak + Use a bigger TeX main memory size to avoid this,\MessageBreak + It is save to continue by pressing <enter>}% + \def\ETC.{\relax}}% + \IfFileExists{\jobname.ent}{% + \endnoteheading + \endnotesize + \@input{\jobname.ent}}{}% + \endgroup } +\def\endnotemark{% + \@ifnextchar[{\@xendnotemark}% + {\stepcounter{endnote}% + \xdef\@theenmark{\theendnote}% + \@endnotemark}} +\def\endnotetext{% + \@ifnextchar[{\@xendnotenext}% + {\xdef\@theenmark{\theendnote}% + \@endnotetext}} +\def\endnoteheading{\section*{\notesname + \imarkboth{\notesname}{\notesname}}\leavevmode\par} +\def\@xendnote[#1]{\begingroup + \c@endnote=#1\relax + \xdef\@theenmark{\theendnote}\endgroup + \@endnotemark\@endnotetext} +\let\@doanendnote=0 +\let\@endanendnote=0 +\newwrite\@endnotes +\newif\if@endnotesopen \@endnotesopenfalse +\def\@openendnotes{% + \if@filesw \immediate\openout\@endnotes=\jobname.ent\relax + \global\@endnotesopentrue \fi} +\long\def\@endnotetext#1{% + \if@endnotesopen \else \@openendnotes \fi + \if@filesw \immediate\write\@endnotes{\@doanendnote{\@theenmark}}\fi + \begingroup + \def\next{#1}% + \newlinechar='40 + \if@filesw \immediate\write\@endnotes{\meaning\next}\fi + \endgroup + \if@filesw \immediate\write\@endnotes{\@endanendnote}\fi + \edef\@currentlabel{\csname p@endnote\endcsname\@theenmark}} +\def\@xendnotemark[#1]{% + \begingroup + \c@endnote #1\relax + \xdef\@theenmark{\theendnote}\endgroup + \@endnotemark} +\def\@endnotemark{% + \leavevmode + \ifhmode \edef\@x@sf{\the\spacefactor}\fi + \@makeenmark + \ifhmode\spacefactor\@x@sf\fi\relax} +\def\@xendnotenext[#1]{% + \begingroup \c@endnote=#1\relax + \xdef\@theenmark{\theendnote}\endgroup + \@endnotetext} +\newenvironment{thebibliography}[1]{% + \sectioncmd*{\refname}\imarkboth{\bibname}{\bibname}% + \footnotesize + \message{\refname} + \def\bibwidthlabel{\releft#1\reright}% + \list{\kapbib@counter}{\kapbib@list} + \let\makelabel\@biblabel + \def\newblock{\hskip .11em plus .33em minus .07em}% + \sloppy + \clubpenalty10000 + \widowpenalty10000 + \sfcode`\.=1000\relax + }{\endlist} +\AtBeginDocument{% + \def\refname{References}% + \def\bibname{References}} +\def\i@oldseries{} +\newlength{\bibhang} +\setlength{\bibhang}{14pt} +\newcommand{\redot}{.} +\newcommand{\releft}{} +\newcommand{\reright}{} +\if@numreferences + \def\coleft{[} + \def\ccright{]} +\else + \def\coleft{(} + \def\ccright{)} +\fi +\def\@cite#1#2{\coleft{#1\if@tempswa , #2\fi}\ccright} +\let\oldcite\cite +\def\numreferences{% + \typeout{KAP -- Numbered references}% + \def\kapbib@counter{\arabic{enumiv}}% + \def\labelsepwidth{1em}% + \def\kapbib@list{% + \setlength{\labelsep}{\labelsepwidth}% + \settowidth{\labelwidth}{\@biblabel{\bibwidthlabel}}% + \setlength{\leftmargin}{\labelwidth}% + \addtolength{\leftmargin}{\labelsep}% + \setlength{\itemindent}{0pt}% + \setlength{\itemsep}{0pt}% + \setlength{\parsep}{0pt}% + \usecounter{enumiv}% + \let\makelabel\kap@biblabel}% + \def\@biblabel##1{\hfill\releft##1\redot\reright}% + \def\@bibitem##1{\item + \def\@tempa{##1}% + \ifx\@tempa\empty + \if@filesw + \immediate\write\@auxout + {\string\bibcite{\thearticle \the\value{\@listctr}}% + {\the\value{\@listctr}}}% + \fi + \else + \if@filesw + \immediate\write\@auxout + {\string\bibcite{\thearticle ##1}{\the\value{\@listctr}}}% + \fi + \fi + \ignorespaces + }% + \def\@lbibitem[##1]##2{% + \def\@biblabel####1{####1}% + \let\makelabel\@biblabel + \def\@tempa{##2}% + \ifx\@tempa\empty + \item[\@biblabel{\hfill\releft + \arabic{\@listctr}\redot\reright}]% + \if@filesw + {\def\protect####1{\string ####1\space}\immediate + \write\@auxout{\string\bibcite{\thearticle \the\value{\@listctr}}% + {\the\value{\@listctr}}}}% + \fi + \else + \item[\@biblabel{\hfill\releft ##1\redot\reright}]% + \if@filesw + {\def\protect####1{\string ####1\space}\immediate + \write\@auxout{\string\bibcite{\thearticle ##2}{##1}}}% + \fi + \fi + \ignorespaces + }% + \let\@internalcite\oldcite + \let\shortcite\@internalcite + \let\citeauthor\@internalcite + \let\citeyear\@internalcite + \let\inlinecite\@internalcite + \let\opencite\@internalcite + \let\cite\@internalcite + \def\citeauthoryear##1##2{}% +\def\@citex[##1]##2{% + \let\@citea\@empty + \@cite{\@for\@citeb:=##2\do + {\@citea\def\@citea{,\penalty\@m\ }% + \if@filesw\immediate\write\@auxout{\string\citation{\@citeb}}\fi + \edef\gl@citeb{\expandafter\@firstofone\@citeb}% + \edef\@citeb{\thearticle\expandafter\@firstofone\@citeb}% + \@ifundefined{b@\@citeb}{% + \@ifundefined{b@\gl@citeb}{% + \mbox{\reset@font\bfseries ?}% + \G@refundefinedtrue + \@latex@warning + {Citation `\@citeb' on page \thepage \space undefined}}% + {\hbox{\csname b@\gl@citeb\endcsname}}}% + {\hbox{\csname b@\@citeb\endcsname}}% + }}{##1}} +} +\def\namedreferences{% + \typeout{KAP -- Named references}% + \def\@bibitem##1{\item + \def\@tempa{##1}% + \ifx\@tempa\empty + \if@filesw \immediate\write\@auxout{% + \string\bibcite{\thearticle ??}{??}}\fi + \else + \if@filesw \immediate\write\@auxout{% + \string\bibcite{\thearticle ##1}{??}}\fi + \fi + \ignorespaces + }% + \def\@lbibitem[##1]##2{\item[\@biblabel{##1}\hfill]% + \def\@tempa{##2}% + \stepcounter{\@listctr}% + \ifx\@tempa\empty + \if@filesw{\def\protect####1{\string ####1\space}\immediate + \write\@auxout{\string\bibcite{\thearticle + \the\value\@listctr}{##1}}}\fi + \else + \if@filesw{\def\protect####1{\string ####1\space}\immediate + \write\@auxout{\string\bibcite{\thearticle ##2}{##1}}}\fi + \fi + \ignorespaces + }% +\def\labelsepwidth{1em}% +\def\kapbib@counter{\relax }% + \def\kapbib@list{% + \setlength{\labelsep}{0em}% + \setlength{\labelwidth}{0pt}% + \setlength{\itemindent}{-\bibhang}% + \setlength{\itemsep}{0pt}% + \setlength{\parsep}{0pt}% + \usecounter{enumiv}% + \setlength{\leftmargin}{\bibhang}% + \i@oldseries + }% + \def\@biblabel##1{}% + \let\@internalcite\oldcite + \def\cite{\@ifstar{\citeyear}{\klu@cite}}% + + \def\klu@cite{\def\@citeseppen{1000}% + \def\@cite####1####2{\coleft{####1\if@tempswa , ####2\fi}\ccright}% + \def\citeauthoryear####1####2{{\rm\i@oldseries ####1, ####2}}\@internalcite }% + + \def\shortcite{\def\@citeseppen{1000}% + \def\@cite####1####2{\coleft{####1\if@tempswa , ####2\fi}\ccright}% + \def\citeauthoryear####1####2{{\rm\i@oldseries ####2}}\@internalcite }% + + \def\citeauthor##1{\def\@citeseppen{1000}% + \def\@cite####1####2{{####1\if@tempswa , ####2\fi}}% + \def\citeauthoryear####1####2{\rm ####1}\@citedata{##1}}% + + \def\citeyear##1{\def\@citeseppen{1000}% + \def\@cite####1####2{{####1\if@tempswa , ####2\fi}}% + \def\citeauthoryear####1####2{{\rm\i@oldseries ####2}}\@citedata{##1}}% + + \def\opencite##1{\citeauthor{##1}, \citeyear{##1}}% + + \def\inlinecite##1{\citeauthor{##1} (\citeyear{##1})}% +\def\@citedata##1{% + \@tempswafalse% + \let\@citea\@empty + \@cite{\@for\@citeb:=##1\do + {\@citea\def\@citea{,\penalty\@citeseppen\ }% + \if@filesw\immediate\write\@auxout{\string\citation{\@citeb}}\fi + \edef\gl@citeb{\expandafter\@firstofone\@citeb}% + \edef\@citeb{\thearticle\expandafter\@firstofone\@citeb}% + \@ifundefined{b@\@citeb}{% + \@ifundefined{b@\gl@citeb}{% + \mbox{\reset@font\bfseries ?}% + \G@refundefinedtrue + \@latex@warning + {Citation `\@citeb' on page \thepage \space undefined}}% + {\csname b@\gl@citeb\endcsname}}% + {\csname b@\@citeb\endcsname}}}{}} +\def\@citex[##1]##2{% + \let\@citea\@empty + \@cite{\@for\@citeb:=##2\do + {\@citea\def\@citea{;\penalty\@citeseppen\ }% + \if@filesw\immediate\write\@auxout{\string\citation{\@citeb}}\fi + \edef\gl@citeb{\expandafter\@firstofone\@citeb}% + \edef\@citeb{\thearticle\expandafter\@firstofone\@citeb}% + \@ifundefined{b@\@citeb}{% + \@ifundefined{b@\gl@citeb}{% + \mbox{\reset@font\bfseries ?}% + \G@refundefinedtrue + \@latex@warning + {Citation `\@citeb' on page \thepage \space undefined}}% + {\csname b@\gl@citeb\endcsname}}% + {\csname b@\@citeb\endcsname}}}{##1}} +\def\citeauthoryear##1##2{\string\citeauthoryear{##1}{##2}}} +%%%%%%%%%%%%%%%%%%%%%%%%% +\if@numreferences + \numreferences +\else + \namedreferences +\fi +\def\trivm@th{% + \ifnum \@itemdepth >0 \topsep\topsepm@th \fi + \ifnum \@enumdepth >0 \topsep\topsepm@th \fi + \trivlist} +\def\endtrivm@th{\endtrivlist %\egroup +} +\newdimen\eqnoindent +\setlength{\eqnoindent}{0pt} +\def\varequation#1{$$ \gdef\curr@vareq{#1}} +\def\endvarequation{\eqno \var@eqnnum $$\global\@ignoretrue } +\def\var@eqnnum{\reset@font\normalcolor (\curr@vareq)} +\def\varleqno{% + \def\@eqnnum{\hbox to .01\p@{}% + \rlap{\reset@font\rmfamily\normalcolor + \hskip -\displaywidth (\theequation)}}% + \def\var@eqnnum{\hbox to .01\p@{}% + \rlap{\reset@font\rmfamily\normalcolor + \hskip -\displaywidth (\curr@vareq)}}% +}% +\def\varfleqn{% + \newdimen\mathindent + \mathindent\leftmargini + \def\varequation##1{% + \@beginparpenalty\predisplaypenalty + \@endparpenalty\postdisplaypenalty + \gdef\curr@vareq{##1}\trivm@th + \item[]\leavevmode + \hbox to\linewidth\bgroup $ \displaystyle + \hskip\mathindent }% + \def\endvarequation{$\hfil \displaywidth\linewidth + \ifdim \eqnoindent =\z@ + \llap{\hbox{\var@eqnnum}}% + \else + \llap{\hbox to 2pc{\var@eqnnum\hss}\kern \displaywidth + \kern -\eqnoindent}% + \fi + \egroup \endtrivm@th}% + \def\[{\relax + \ifmmode\@badmath + \else + \begin{trivm@th}% + \@beginparpenalty\predisplaypenalty + \@endparpenalty\postdisplaypenalty + \item[]\leavevmode + \hbox to\linewidth\bgroup $\m@th\displaystyle %$ + \hskip\mathindent\bgroup + \fi}% + \def\]{\relax + \ifmmode + \egroup $\hfil% $ + \egroup + \end{trivm@th}% + \else \@badmath + \fi}% + \renewenvironment{equation}{% + \@beginparpenalty\predisplaypenalty + \@endparpenalty\postdisplaypenalty + \refstepcounter{equation}% + \trivm@th + \item[]\leavevmode + \hbox to\linewidth\bgroup $\m@th% $ + \displaystyle + \hskip\mathindent}%%%%%%% + {$\hfil % $ + \displaywidth\linewidth + \ifdim \eqnoindent =\z@ + \llap{\hbox{\@eqnnum}}% + \else + \llap{\hbox to 2pc{\@eqnnum\hss}\kern \displaywidth + \kern -\eqnoindent}% + \fi + \egroup + \endtrivm@th}% + \renewenvironment{eqnarray}{% + \stepcounter{equation}% + \def\@currentlabel{\p@equation\theequation}% + \global\@eqnswtrue\m@th + \global\@eqcnt\z@ + \tabskip\mathindent + \let\\=\@eqncr + \setlength{\abovedisplayskip}{\topsep}% + \ifvmode + \addtolength{\abovedisplayskip}{\partopsep}% + \fi + \addtolength{\abovedisplayskip}{\parskip}% + \setlength{\belowdisplayskip}{\abovedisplayskip}% + \setlength{\belowdisplayshortskip}{\abovedisplayskip}% + \setlength{\abovedisplayshortskip}{\abovedisplayskip}% + $$\everycr{}\halign to\linewidth% $$ + \bgroup + \hskip\@centering + $\displaystyle\tabskip\z@skip{####}$\@eqnsel&% + \global\@eqcnt\@ne \hskip \tw@\arraycolsep \hfil${####}$\hfil&% + \global\@eqcnt\tw@ \hskip \tw@\arraycolsep + $\displaystyle{####}$\hfil \tabskip\@centering&% + \global\@eqcnt\thr@@ + \llap \bgroup + \ifdim \eqnoindent =\z@ \else + \hbox to 2pc \bgroup \fi + ####\ifdim \eqnoindent =\z@ + \egroup \else \hss\egroup\kern \displaywidth + \kern -\eqnoindent\egroup + \fi \tabskip\z@skip\cr}% + {\@@eqncr + \egroup + \global\advance\c@equation\m@ne$$% $$ + \global\@ignoretrue + }} +\def\subequation{\@ifnextchar[{\@subequation}{\@subequation[alph]}} +\def\@subequation[#1]{\refstepcounter{equation}% + \def\@testoption{arabic}% + \def\@testparam{#1}% + \edef\old@equation{\the\c@equation}% + \edef\old@theequation{\theequation}% + \setcounter{equation}{0}% + \ifx\@testoption\@testparam + \def\theequation{\old@theequation.\csname #1\endcsname{equation}}% + \else + \def\theequation{\old@theequation\csname #1\endcsname{equation}}% + \fi} +\def\endsubequation{% + \setcounter{equation}{\old@equation}% + \global\@ignoretrue +} +\newif\if@novspace +\let\@thmscase\uppercase +\newdimen\theoremsep +\theoremsep\z@ +\def\thmdot{.} +\def\@stylehead{\rm } +\def\@styletext{\em } +\let\@dispcase\relax +\newdimen\dispsep +\dispsep\parindent +\def\dispdot{.} +\def\@disphead{\it } +\def\@disptext{\rm } + +\def\pr@@f#1{% + \par + \if@novspace \vskip-\lastskip + \else \addvspace{1\baselineskip + \@plus 0.5\baselineskip \@minus 0.1\baselineskip}% + \fi \indent + {\it #1.\/} \ignorespaces +} +\def\endpr@@f{% + \par + \addvspace{1\baselineskip \@plus 0.5\baselineskip \@minus + 0.1\baselineskip}% + \global\@novspacefalse +} + +\def\newproof#1#2{% + \expandafter\def\csname #1\endcsname{\pr@@f{#2}}% + \expandafter\def\csname end#1\endcsname{\endpr@@f}} +\newproof{pf}{Proof} + +\newenvironment{pf*}[1]{\pr@@f{#1}}{\endpr@@f} +\def\qed{\relax + \ifmmode + ~\hfill\Box + \else + \unskip\nobreak ~\hfill$\Box$% + \fi \par} +\newlength\items@ve\newlength\labels@ve +\def\@begintheorem#1#2{% + \items@ve=\itemindent \labels@ve=\labelsep + \trivlist + \global\@novspacetrue \itemindent\theoremsep + \item[\kern\labelsep + {\@stylehead\@thmscase{#1}\ #2\thmdot\/}]\ \@styletext + \itemindent=\items@ve \labelsep=\labels@ve} +\def\@opargbegintheorem#1#2#3{% + \items@ve=\itemindent \labels@ve=\labelsep + \trivlist \labelsep\z@ + \global\@novspacetrue \itemindent\theoremsep + \item[\kern \labelsep {\@stylehead\@thmscase{#1}\ #2\ + (#3). \/}]\ \@styletext + \itemindent=\items@ve \labelsep=\labels@ve} +\def\@endtheorem{\endtrivlist} +\def\rmtheorem#1{% + \expandafter\g@addto@macro\csname #1\endcsname{\rmfamily\upshape }% + } +\def\newdisplay#1{\@ifnextchar[{\@odisp{#1}}{\@ndisp{#1}}} +\def\@ndisp#1#2{% + \@ifnextchar[{\@xndisp{#1}{#2}}{\@yndisp{#1}{#2}}} +\def\@xndisp#1#2[#3]{\expandafter\@ifdefinable\csname #1\endcsname + {\@definecounter{#1}\@newctr{#1}[#3]% + \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand + \csname the#3\endcsname \@dispcountersep \@dispcounter{#1}}% +\global\@namedef{#1}{% + \@disp{#1}{#2}}\global\@namedef{end#1}{\@enddisplay}}} +\def\@yndisp#1#2{\expandafter\@ifdefinable\csname #1\endcsname +{\@definecounter{#1}% +\expandafter\xdef\csname the#1\endcsname{\@dispcounter{#1}}% +\global\@namedef{#1}{% + \@disp{#1}{#2}}\global\@namedef{end#1}{\@enddisplay}}} +\def\@odisp#1[#2]#3{% + \@ifundefined{c@#2}{\@nocounterr{#2}}% + {\expandafter\@ifdefinable\csname #1\endcsname + {\global\@namedef{the#1}{\@nameuse{the#2}}% +\global\@namedef{#1}{\@disp{#2}{#3}}% +\global\@namedef{end#1}{\@enddisplay}}}} +\def\@disp#1#2{\refstepcounter + {#1}\@ifnextchar[{\@ydisp{#1}{#2}}{\@xdisp{#1}{#2}}} +\def\@xdisp#1#2{\@begindisplay{#2}{\csname the#1\endcsname}\ignorespaces} +\def\@ydisp#1#2[#3]{\@opargbegindisplay{#2}{\csname + the#1\endcsname}{#3}\ignorespaces} +\def\@dispcounter#1{\noexpand\arabic{#1}} +\def\@dispcountersep{.} +\def\@begindisplay#1#2{% + \items@ve=\itemindent \labels@ve=\labelsep + \trivlist + \global\@novspacefalse \itemindent\dispsep + \item[{\@disphead + \@dispcase{#1}\ #2\dispdot \/}]\@disptext + \itemindent=\items@ve \labelsep=\labels@ve} +\def\@opargbegindisplay#1#2#3{% + \items@ve=\itemindent \labels@ve=\labelsep + \trivlist + \global\@novspacefalse + \itemindent \dispsep + \item[{\@disphead \@dispcase{#1}\ #2\dispdot\ + (\@dispcase{#3})\/}]\@disptext + \itemindent=\items@ve \labelsep=\labels@ve} +\def\@enddisplay{\endtrivlist} +\if@thms + \newtheorem{thm}{THEOREM} + \newtheorem{cor}[thm]{COROLLARY} + \newtheorem{lem}[thm]{LEMMA} + \newtheorem{claim}[thm]{CLAIM} + \newtheorem{conj}[thm]{CONJECTURE} + \newtheorem{prop}[thm]{PROPOSITION} + \newtheorem{exer}[thm]{EXERCISE} + \newtheorem{REM}[thm]{REMARK} + \newtheorem{prob}[thm]{PROBLEM} + \newtheorem{alg}{ALGORITHM} + \rmtheorem{alg} + \newtheorem{defn}[thm]{DEFINITION} + \rmtheorem{defn} + \newtheorem{exmp}[thm]{EXAMPLE} + \rmtheorem{exmp} + \newdisplay{crit}{Criterion} + \newdisplay{rem}{Remark} + \newdisplay{Note}{Note} + \newdisplay{summ}{Summary} + \newdisplay{case}{Case} +\fi +\arraycolsep = 3pt +\@EndKlumathook +\newcommand{\part}{% + \cleardoublepage + \thispagestyle{part}% + \hbox{}\vskip 2in + \secdef\@part\@spart} +\def\@part[#1]#2{% + \ifnum \c@secnumdepth >-2\relax + \refstepcounter{part}% + \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}% + \else + \addcontentsline{toc}{part}{#1}% + \fi + \imarkboth{}{}% + {\centering + \ifnum \c@secnumdepth >-2\relax + \huge\bf \partname\ \thepart + \par + \vskip 20pt + \fi + \Huge \bf #1\par + }% + \@endpart + } + +\def\@spart#1{{\centering\Huge \bf #1\par}\@endpart} +\def\@endpart{\vfil\cleardoublepage} +\def\partname{Part} +\let\ps@part\ps@empty + +\if@chapterdef + + % + % Typeset text and number. + % + \newcommand{\@makechapterhead}[2]{\vspace*{\Cspaceabove}% + {\parindent 0pt \hyphenpenalty 10000 + \Cflushstyle \Cnumstyle + \Chang{#1}% + \Ctextstyle \Ccase{#2}\par + \nobreak \Cspaceafter \relax + }} + + \newcommand{\chapter}{% + \if@openright + \cleardoublepage + \else + \clearpage + \fi + \thispagestyle{chapter}% + \global\@topnum\z@ + \@afterindentfalse + \secdef\@chapter\@schapter + } + \def\@chapter[#1]#2{% + \ifnum \c@secnumdepth >\m@ne + \refstepcounter{chapter}% + \message{\@chapapp\space\thechapter\chapterdot}% + \addcontentsline{toc}{chapter}{\protect + \numberline{\thechapter}#1}% + \else + \addcontentsline{toc}{chapter}{#1}% + \fi + \chaptermark{#1}% + \addtocontents{lof}{\protect\addvspace{10pt}}% + \addtocontents{lot}{\protect\addvspace{10pt}}% + \@makechapterhead{\thechapter\chapterdot\ }{#2}% + \@afterheading + } + \newcommand{\@schapter}[1]{\@makechapterhead{}{#1} \@afterheading} + + \newcommand{\Chang}[1]{#1} + \newcommand{\Cspaceabove}{33pt} + \newcommand{\Cspaceafter}{\vskip 33pt} + \newcommand{\Cflushstyle}{\centering} + \newcommand{\Cnumstyle}{\large\rm} + \newcommand{\Ctextstyle}{} + \newcommand{\Ccase}[1]{#1} + \newcommand{\@chapapp}{\chaptername} + \newcommand{\chapterdot}{.} + \let\ps@chapter\ps@empty +\fi +\newcommand{\vsecspace}[1]{% + \if@nobreak\else + \vskip #1\relax \fi} +\def\Shaveatleast{5\baselineskip} +\def\SShaveatleast{4\baselineskip} +\def\SSShaveatleast{4\baselineskip} +\newcommand{\@haveatleast}[1]{\relax\par \vskip #1 + \penalty 0\vskip -#1 \relax } +\def\@Xsect{% + \global\@nobreakfalse + \global\@noskipsectrue + \everypar{\setbox0\lastbox + \global\@noskipsecfalse + \begingroup \@Svsechd \endgroup + \everypar{}% + }} +\newcommand{\Forcedhang}[1]{\leavevmode + \setbox0=\hbox{#1}\hangindent\wd0 + \hangafter=1 \box0 } +\def\contentsname{Table of Contents}% +\def\listfigurename{List of Figures}% +\def\listtablename{List of Tables}% +\def\chaptername{Chapter}% +\def\sectionname{Section}% +\def\appendixname{Appendix}% +\newcommand{\@makesectionhead}[2]{\vsecspace{\Sspaceabove}% + {\parindent0pt \hyphenpenalty=10000 \baselineskip12pt + \Sflushstyle \Snumstyle + \Shang{#1}% + \Stextstyle \Scase{#2}\par + \nobreak \Sspaceafter \relax + }} + +\newcommand{\section}{\@haveatleast{\Shaveatleast + }\@afterindentfalse \secdef\@section\@ssection} + +\def\@section[#1]#2{% + \ifnum \c@secnumdepth >\z@ + \refstepcounter{section}% + \addcontentsline{toc}{section}{\protect \numberline{\thesection}#1}% + \else + \addcontentsline{toc}{section}{#1}% + \fi + \sectionmark{#1}% + \@makesectionhead{\thesection\sectiondot\hskip 0.7em}{#2}% + \@afterheading + } + +\def\@ssection#1{\@makesectionhead{}{#1}\@afterheading} + +\newcommand{\Shang}[1]{\Forcedhang{#1}} +\newcommand{\Sflushstyle}{\centering} +\newcommand{\Snumstyle}{\normalsize\bf} +\newcommand{\Stextstyle}{} +\newcommand{\Sspaceabove}{2\baselineskip plus6pt minus4pt} +\newcommand{\Sspaceafter}{\vskip 1\baselineskip plus3pt minus2pt} +\newcommand{\Scase}[1]{#1} +\newcommand{\sectiondot}{.} +\newcommand{\@makesubsectionhead}[2]{\vsecspace{\SSspaceabove}% + {\parindent0pt \hyphenpenalty=10000 \baselineskip12pt + \SSflushstyle \SSnumstyle + \SShang{#1}% + \SStextstyle \SScase{#2}\par + \nobreak \SSspaceafter \relax + }} + +\newcommand{\subsection}{\@haveatleast{\SShaveatleast}% + \@afterindentfalse \secdef\@subsection\@ssubsection + } + +\def\@subsection[#1]#2{% + \ifnum \c@secnumdepth >\@ne + \refstepcounter{subsection}% + \addcontentsline{toc}{subsection}{\protect + \numberline{\thesubsection}#1}% + \else + \addcontentsline{toc}{subsection}{#1}% + \fi + \subsectionmark{#1} + \@makesubsectionhead{\thesubsection\sectiondot\hskip 0.7em}{#2}% + \@afterheading + } +\def\@ssubsection#1{\@makesubsectionhead{}{#1}\@afterheading} + +\newcommand{\SShang}[1]{\Forcedhang{#1}} +\newcommand{\SSflushstyle}{\raggedright} +\newcommand{\SSnumstyle}{\normalsize\rm} +\newcommand{\SStextstyle}{\sc} +\newcommand{\SSspaceabove}{1\baselineskip plus3pt minus2pt} +\newcommand{\SSspaceafter}{\vskip .8\baselineskip plus2pt minus2pt} +\newcommand{\SScase}[1]{#1} +\newcommand{\@makesubsubsectionhead}[2]{\vsecspace{\SSSspaceabove}% + {\parindent0pt \hyphenpenalty=10000 \baselineskip12pt + \SSSflushstyle \SSSnumstyle + \SSShang{#1}% + \SSStextstyle \SSScase{#2}\par + \nobreak \SSSspaceafter \relax + }} + +\newcommand{\subsubsection}{\@haveatleast{\SSShaveatleast + }\@afterindentfalse + \secdef\@subsubsection\@ssubsubsection} +\def\@subsubsection[#1]#2{% + \ifnum \c@secnumdepth >2 + \refstepcounter{subsubsection} + \addcontentsline{toc}{subsubsection}{\protect + \numberline{\thesubsubsection}#1}% + \else + \addcontentsline{toc}{subsubsection}{#1}% + \fi + \subsubsectionmark{#1} + \@makesubsubsectionhead{\thesubsubsection\sectiondot\hskip0.7em}{#2}% + \@afterheading + } +\def\@ssubsubsection#1{\@makesubsubsectionhead{}{#1}\@afterheading} + +\newcommand{\SSShang}[1]{\Forcedhang{#1}} +\newcommand{\SSSflushstyle}{\raggedright} +\newcommand{\SSSnumstyle}{\normalsize\rm} +\newcommand{\SSStextstyle}{\it} +\newcommand{\SSSspaceabove}{1\baselineskip plus3pt minus2pt} +\newcommand{\SSSspaceafter}{\vskip 1sp} +\newcommand{\SSScase}[1]{#1} +\newcommand{\@makeparagraphhead}[2]{% + \vsecspace{\Pspaceabove }% + \def\@Svsechd{% + {\Pflushstyle \Pnumstyle + \Phang{#1}% + \Ptextstyle \Pcase{#2}% + \Pspaceafter \relax }}\@Xsect + } + +\newcommand{\paragraph}{\par \@afterindentfalse + \secdef\@paragraph\@sparagraph } + +\def\@paragraph[#1]#2{% + \ifnum \c@secnumdepth >3 + \refstepcounter{paragraph}% + \addcontentsline{toc}{paragraph}{\protect + \numberline{\theparagraph}#1}% + \else + \addcontentsline{toc}{paragraph}{#1}% + \fi + \paragraphmark{#1}% + \@makeparagraphhead{\theparagraph\sectiondot\hskip 0.7em}{#2}% + } +\def\@sparagraph#1{\@makeparagraphhead{}{#1}} + +\newcommand{\Pspaceabove}{1\baselineskip plus3pt minus2pt} +\newcommand{\Phang}[1]{#1} +\newcommand{\Pflushstyle}{} +\newcommand{\Pnumstyle}{\normalsize\rm} +\newcommand{\Ptextstyle}{\it} +\newcommand{\Pcase}[1]{#1} +\newcommand{\Pspaceafter}{\hskip 1em} +\newcommand{\@makesubparagraphhead}[2]{% + \vskip \SPspaceabove + \def\@Svsechd{% + {\SPflushstyle \SPnumstyle + \SPhang{#1}% + \SPtextstyle \SPcase{#2}% + \SPspaceafter \relax}}\@Xsect + } +\newcommand{\subparagraph}{\par\@afterindentfalse + \secdef\@subparagraph\@ssubparagraph } + +\def\@subparagraph[#1]#2{% + \ifnum \c@secnumdepth >4 + \refstepcounter{subparagraph}% + \addcontentsline{toc}{subparagraph}{\protect + \numberline{\thesubparagraph}#1}% + \else + \addcontentsline{toc}{subparagraph}{#1}% + \fi + \paragraphmark{#1}% + \@makesubparagraphhead{\thesubparagraph\sectiondot\hskip 0.7em}{#2}% + } +\def\@ssubparagraph#1{\@makesubparagraphhead{}{#1}} + +\newcommand{\SPspaceabove}{1\baselineskip plus3pt minus2pt} +\newcommand{\SPhang}[1]{} +\newcommand{\SPflushstyle}{} +\newcommand{\SPnumstyle}{\normalsize\rm} +\newcommand{\SPtextstyle}{\it} +\newcommand{\SPcase}[1]{#1} +\newcommand{\SPspaceafter}{\hskip 1em} +\newcounter{part} +\renewcommand{\thepart}{\Roman{part}} +\if@chapterdef + \newcounter{chapter} + \renewcommand{\thechapter}{\arabic{chapter}} + \newcounter{section}[chapter] + \renewcommand{\thesection}{\thechapter.\arabic{section}} +\else + \newcounter{section} + \renewcommand{\thesection}{\arabic{section}} +\fi +\newcounter{subsection}[section] +\newcounter{subsubsection}[subsection] +\newcounter{paragraph}[subsubsection] +\newcounter{subparagraph}[paragraph] +\renewcommand{\thesubsection}{\thesection.\arabic{subsection}} +\renewcommand{\thesubsubsection}{\thesubsection.\arabic{subsubsection}} +\renewcommand{\theparagraph}{\thesubsubsection.\arabic{paragraph}} +\renewcommand{\thesubparagraph}{\theparagraph.\arabic{subparagraph}} +\def\@pnumwidth{1.55em} +\def\@tocrmarg{2.55em} +\def\@dotsep{10000} + +\setcounter{tocdepth}{2} +\setcounter{secnumdepth}{4} +\def\tableofcontents{\sectioncmd *{\contentsname}% + \imarkboth{\contentsname}{\contentsname}% + \message{\contentsname}% + \@starttoc{toc}\newpage} +\def\listoffigures{\sectioncmd *{\listfigurename}\imarkboth + {\listfigurename}{\listfigurename}% + \message{\listfigurename}% + \@starttoc{lof}} +\def\listoftables{\sectioncmd *{\listtablename}\imarkboth + {\listtablename}{\listtablename}% + \message{\listtablename}% + \@starttoc{lot}} + +\def\l@figure{\@dottedtocline{1}{1.5em}{2.3em}} +\let\l@table\l@figure + +\def\l@part#1#2{% + \addpenalty{-\@highpenalty} + \addvspace{2.25em plus 1pt} + \begingroup + \@tempdima 3em + \parindent \z@ \rightskip \@pnumwidth + \parfillskip -\@pnumwidth + {\large \bf + \leavevmode + #1\hfil \hbox to\@pnumwidth{\hss #2}}\par + \nobreak + \global\@nobreaktrue + \everypar{\global\@nobreakfalse\everypar{}} + \endgroup + } + +\def\l@chapter#1#2{\addpenalty{-\@highpenalty} + \vskip 1.0em plus 1pt + \@tempdima 1.5em + \begingroup + \parindent \z@ \rightskip \@pnumwidth + \parfillskip -\@pnumwidth + \bf + \leavevmode + \advance\leftskip\@tempdima + \hskip -\leftskip + #1\nobreak\hfil \nobreak\hbox to\@pnumwidth{\hss #2}\par + \penalty\@highpenalty + \endgroup + } + +\def\l@section{\@dottedtocline{1}{1.5em}{2.3em}} +\def\l@subsection{\@dottedtocline{2}{3.8em}{3.2em}} +\def\l@subsubsection{\@dottedtocline{3}{7.0em}{4.1em}} +\def\l@paragraph{\@dottedtocline{4}{10em}{5em}} +\def\l@subparagraph{\@dottedtocline{5}{12em}{6em}} +\newif\if@mainmatter \@mainmattertrue +\if@chapterdef + \newcommand{\appendix}{\par + \@mainmatterfalse + \setcounter{chapter}{0}% + \setcounter{section}{0}% + \renewcommand{\thechapter}{\Alph{chapter}}% + \renewcommand{\@chapapp}{\appendixname}% + \message{\appendixname}% + } +\else + \newcommand{\appendix}{\par + \section*{Appendix}% + \setcounter{section}{0}% + \setcounter{subsection}{0}% + \renewcommand{\thesection}{\Alph{section}}% + \message{\appendixname}% + } +\fi + +\newenvironment{theindex}{% + \columnseprule \z@ + \columnsep \indexsep + \if@chapterdef + \twocolumn[\@makechapterhead{}{\indexname}] + \addcontentsline{toc}{chapter}{\indexname}% + \else + \twocolumn[\@makesectionhead{}{\indexname}] + \addcontentsline{toc}{section}{\indexname}% + \fi + \imarkboth{\indexname}{\indexname}% + \message{\indexname}% + \thispagestyle{index}% + \parindent\z@ + \parskip\z@ plus .3pt\relax + \let\item\@idxitem \indexfont + }{\onecolumn} +\def\indexfont{\footnotesize} +\let\ps@index\ps@empty +\def\@idxitem{\par\hangindent 36pt} +\def\subitem{\par\hangindent 36pt \hspace*{12pt}} +\def\subsubitem{\par\hangindent 36pt \hspace*{24pt}} +\def\indexspace{\par \vskip 10pt plus 5pt minus 3pt\relax} +\def\indexsep{24pt} + + + + + +\@kaplisttrue + +\AtBeginDocument{\let\sectioncmd\section} +\AtBeginDocument{\let\imarkboth\@gobbletwo} + +\def\@date{\vskip \afterdateskip } % no default dates + +\renewcommand{\fnum@figure}{{\itshape\figurename~\thefigure\figtabdot\/}} +\renewcommand{\thetable}{\Roman{table}} +\indentedcaptions + +\def\Uppercase#1{#1} +\setlength\textheight{559pt} +\setlength\textwidth{28pc} +\setlength\marginparwidth{0pt} +\setlength\lineskip{1\p@} +\setlength\normallineskip{1\p@} +\renewcommand\baselinestretch{} +\@lowpenalty 51 +\@medpenalty 151 +\@highpenalty 301 +\@beginparpenalty -\@lowpenalty +\@endparpenalty -\@lowpenalty +\@itempenalty -\@lowpenalty +\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm} +\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf} +\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt} +\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf} +\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit} +\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl} +\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc} +\providecommand{\cal}{\protect\pcal} +\newcommand{\pcal}{\@fontswitch{\relax}{\mathcal}} +\providecommand{\mit}{\protect\pmit} +\newcommand{\pmit}{\@fontswitch{\relax}{\mathnormal}} +\setlength\tabbingsep{\labelsep} +\clubpenalty=10000 +\widowpenalty=10000 +%%%%%%% +\def\kapmathindent{14pt} +\pagestyle{headings} +\pagenumbering{arabic} +\frenchspacing +\endinput +%% +%% End of file `kluwer.cls'. diff --git a/papers/cfrontend_new/macros.tex b/papers/cfrontend_new/macros.tex new file mode 100644 index 0000000..26ff6cb --- /dev/null +++ b/papers/cfrontend_new/macros.tex @@ -0,0 +1,146 @@ + +%\newcommand{\xxx}[1]{{\color{BrickRed}{#1}}} +%\newcommand{\xxx}[1]{\marginpar{\footnotesize\color{red}{#1}}} +\newcommand{\xxx}{} +\newcommand{\comment}{} +\newcommand{\cminor}{Cminor} +\newcommand{\compcert}{CompCert} + +\newcommand{\defeq}{=_{\mathrm{def}}} +% Abbreviations + +% \newtheorem{thm}{Theorem}[section] +% \newtheorem{lemma}[thm]{Lemma} +% \newtheorem{corollary}[theorem]{Corollary} + +% \newtheorem{dfn}[theorem]{Definition} +% \newtheorem{definition}[theorem]{Definition} + +% Operators, relations, etc. + +\def\seq#1{#1^*} +\def\opt#1{#1^?} +\def\some#1{\lfloor #1 \rfloor} +\def\Clight{{Clight{}}} +\def\tr{{\it tr}} +\def\vg{{\it lv}} +\def\ls{\it ls} +\def\ofs{{\it ofs}} +\def\op{{\it op}} +\def\chunk{\kappa} %{\it chunk}} +\def\sig{{\sigma}} +\def\fn{{\it def{\char95}fn}} +\def\cfn{{\it fn}} +\def\prog{{\it prog}} +\def\evv{{\it ev}} +\def\ev{{\it e}} +\def\tr{{\it tr}} +\def\E0{{\it \emptyset_\tr}} +\def\fl{{\it fl}} +\def\cenv{\gamma} +\def\tcast#1#2{{\cal C}_{#1}^{#2}} +\def\tcasta{{\cal C}_1} +\def\tcastb{{\cal C}_2} +\def\tlval{{\cal L}} +\def\trval{{\cal R}} +\def\tstmt{{\cal S}} +\def\tfunction{{\cal F}} +\def\valinj#1{\stackrel{#1}{\approx}} +\def\meminj#1{\stackrel{#1}{\approx}} +\def\outinj#1#2{\stackrel{#1,#2}{\approx}} +\def\loc{{\it loc}} +\def\envmatch{{\it EnvMatch}} +\def\csmatch{{\it CallInv}} +\def\sp{{\it sp}} +\def\cs{{\it cs}} +\def\evallvalue{\stackrel{l}{\Rightarrow}} +\def\evalexpr{\Rightarrow} +\def\evalstmt{\Rightarrow} +\def\evalfunc{\stackrel{f}{\Rightarrow}} +\def\evalprog{\Rightarrow} +%\def\evalexpr2{\rightarrow} +%\def\evalstmt2{\rightarrow} +%\def\evalfunc2{\rightarrow} +%\def\evalprog2{\rightarrow} +\def\inj{\alpha} +\def\accessmode{{\cal A}} + +\newcommand{\sbcm}[1]{\textcolor{red}{\textit{#1}}} +\newcommand{\guardbox}{\raisebox{1pt}{\makebox[0pt][l]{\(\sqcap\)}}{\raisebox{-1pt}{\(\sqcup\)}}} +\newcommand{\danscarre}[2]{ \makebox[0pt][l]{\scriptsize \hspace{1pt}#1}{\guardbox{}^{#2}} } +\newcommand{\unannot}[2]{{\underline{#1}}^{#2}} +%\newcommand{\unannot}[2]{\mbox{\fbox{#1}\textsuperscript{#2}}} +%\newcommand{\unannot}[2]{\danscarre{#1}{#2}} + + +\newcommand{\tyface}[1]{\ensuremath{\mathsf{#1}}} + +\newcommand{\option}{\tyface{option}} +\newcommand{\val}{\tyface{val}} +\newcommand{\Vundef}{\tyface{Vundef}} +\newcommand{\Vint}{\tyface{Vint}} +\newcommand{\Vfloat}{\tyface{Vfloat}} +\newcommand{\Vptr}{\tyface{Vptr}} +\newcommand{\expr}{\tyface{expr}} +\newcommand{\env}{\tyface{env}} +\newcommand{\mem}{\tyface{mem}} +\newcommand{\exprlist}{\tyface{exprlist}} +\newcommand{\Some}{\tyface{Some}} +\newcommand{\None}{\tyface{None}} +\newcommand{\Eval}{\tyface{Eval}} +\newcommand{\Evar}{\tyface{Evar}} +\newcommand{\Eop}{\tyface{Eop}} +\newcommand{\Eload}{\tyface{Eload}} +\newcommand{\Econdition}{\tyface{Econdition}} +\newcommand{\Elet}{\tyface{Elet}} +\newcommand{\Eletvar}{\tyface{Eletvar}} +\newcommand{\Enil}{\tyface{Enil}} +\newcommand{\Econs}{\tyface{Econs}} +\newcommand{\Sassign}[2]{#1:=#2} +\newcommand{\Sstore}[3]{\tyface{[}#2\tyface{]}_{#1}\tyface{:=}#3} +\newcommand{\Scall}[4]{\tyface{call}\,#1\,#3\,#4} +\newcommand{\Sif}[3]{\tyface{if}\,#1\,\tyface{then}\,#2\,\tyface{else}\,#3} +\newcommand{\Sloop}[1]{\tyface{loop}\,#1} +\newcommand{\Sblock}[1]{\tyface{block}\,#1} +\newcommand{\Sexit}[1]{\tyface{exit}\,#1} +\newcommand{\Sreturn}[1]{\tyface{return}\,#1} +\newcommand{\Sseq}[2]{#1;#2} +\newcommand{\Sskip}{\tyface{skip}} + +\newcommand{\spt}{\ensuremath{\mathit{sp}}} +\newcommand{\stmt}{\tyface{stmt}} +\newcommand{\id}{\ensuremath{\mathit{id}}} +\newcommand{\out}{\ensuremath{\mathit{out}}} +\newcommand{\outcome}{\tyface{outcome}} +\newcommand{\outn}{\tyface{Out_{normal}}} +\newcommand{\oute}[1]{\tyface{Out_{exit}\,#1}} +\newcommand{\outr}[1]{\tyface{Out_{return}\,#1}} + +\newcommand{\updrho}[2]{\tyface{update_{rho}}(#1,#2)} +\newcommand{\updmem}[2]{\tyface{update_{mem}}(#1,#2)} +\newcommand{\updsp}[2]{\tyface{update_{sp}}(#1,#2)} +\newcommand{\updphi}[2]{\tyface{update_{phi}}(#1,#2)} +\newcommand{\strho}[1]{\tyface{get_{rho}}(#1)} +\newcommand{\stmem}[1]{\tyface{get_{mem}}(#1)} +\newcommand{\stsp}[1]{\tyface{get_{sp}}(#1)} + +%\newcommand{\evalexpr}[8]{#1;(#2;#3;#4;#5;#6) \vdash #7 \Downarrow #8} +%\newcommand{\evalexp}[3]{\fmap; #1 \vdash #2 \Downarrow #3} +\newcommand{\evaloperation}[5]{#1;#2 \vdash #3(#4) \Downarrow_\tyface{eval\_operation} #5} +\newcommand{\execstmts}[8]{#1;(#2;#3;#4) \Downarrow_#5 (#6;#7;#8)} +\newcommand{\execstmt}[4]{(#2,#1) \Downarrow_#3 #4} +\newcommand{\execstmtk}[5]{(#2,\Kseq{#1}{#3}) \Downarrow_{#4} #5} +\newcommand{\execpgm}[2]{\vdash #1 \Downarrow #2} + +\newcommand{\loadv}[4]{#1\vdash #2\stackrel{#3}{\mapsto}#4} +\newcommand{\storev}[5]{#5=#2[#3\stackrel{#1}{:=}#4]} +\newcommand{\agree}{\approx} +\newcommand{\safe}[1]{\tyface{safe}\,#1} +\newcommand{\cat}[2]{#1 \circ #2} + +\newcommand{\ceq}[3]{#2\stackrel{#1}{\mbox{\texttt{==}}}#3} +\newcommand{\ieq}[2]{\ceq{\mathrm{int}}{#1}{#2}} + +\newcommand{\nomem}[1]{\lfloor{#1}\rfloor} +\newcommand{\withmem}[2]{\lceil{#1}\rceil^{#2}} + diff --git a/papers/cfrontend_new/mymacros.sty b/papers/cfrontend_new/mymacros.sty new file mode 100755 index 0000000..9b2df82 --- /dev/null +++ b/papers/cfrontend_new/mymacros.sty @@ -0,0 +1,221 @@ +% First, second, third, n-th, premier, second, n-ieme + +\def\th{^{\mbox{\scriptsize th}}} +\def\st{^{\mbox{\scriptsize st}}} +\def\nd{^{\mbox{\scriptsize nd}}} +\def\rd{^{\mbox{\scriptsize rd}}} +\def\ier{^{\mbox{\scriptsize ier}}} +\def\iere{^{\mbox{\scriptsize i\`ere}}} +\def\ieme{^{\mbox{\scriptsize i\`eme}}} +\def\eme{^{\mbox{\scriptsize e}}} + +% e.g., i.e., et al. +\def\eg{e.g.\ } +\def\ie{i.e.\ } +\def\vs{vs.\ } +\def\etal{{\em et al.}\ } + +% Theorem environments + +\newtheorem{prop}{Proposition} +\ifx\proof\undefined% Some styles, e.g. jfp.sty, already provide a "proof" env. +\def\proof{\trivlist \item[\hskip\labelsep {\bf Proof:}]} +\def\endproof{\hspace*{0pt plus 1fill}$\Box$\endtrivlist} +\fi +%% \ifx\example\undefined +%% \def\example{\trivlist \item[\hskip\labelsep {\bf Example:}]} +%% \def\endexample{\hspace*{0pt plus 1fill}$\Box$\endtrivlist} +%% \fi +\def\case#1.{\medskip\noindent {\bf Case} #1.} +\def\cas#1.{\medskip\noindent {\bf Cas} #1.} +\def\andalso{\quad\mbox{and}\quad} + +% Alternate names for various math stuff + +\def\alt{\mid} % `or' in a grammar +\def\dot{.\,} % for proper spacing in lambda terms +\let\syntequal=\equiv % three-line equal +\def\equiv{\approx} % wavy equal +\def\epsilon{\varepsilon} % Good-looking epsilon +\def\phi{\varphi} % Good-looking phi +\def\reduce{\stackrel{*}{\rightarrow}} % Reduction relation +\def\fun{\rightarrow} % Function type +\def\Fun{\Rightarrow} % Function kinds +\def\becomes{\leftarrow} % In substitutions +\def\Dom{{\rm Dom}} +\def\Im{{\rm Rng}} +\def\inter{\cap} +\def\biginter{\bigcap} +\def\union{\cup} +\def\bigunion{\bigcup} +\def\ttSigma{\hbox{\tt\char6}} % Sigma in typewriter font +\def\rond{\circ} % Function composition +\def\sem{\models} % |= + +% Denotational brackets +\def\den#1{[\![#1]\!]} + +% For syntax definitions +% \begin{syntax} +% left-hand side & ::= & right-hand side & comment \\ +% & \alt & more right-hand side & more comment +% \end{syntax} +% Use \syntaxclass{Foo} to insert a title line above a syntax definition. +% Do not put \\ before \end{syntax} or \syntaxclass{...} +% Use \begin{syntaxleft} ... \end{syntaxleft} to insert the title +% lines to the left of the definitions. + +\def\syntaxvspace{\medskip} + +\def\syntax{ +\par\syntaxvspace\goodbreak\noindent +\bgroup +\let\\=\cr +\interlinepenalty=50 % discourage page breaks in a definition +\global\let\syntaxclass=\firstsyntaxclass +\if@twocolumn +\halign\bgroup~~$##$&\hfil${}##{}$&$##$~\hfil&##\hfil\cr +\else +\halign\bgroup\qquad\qquad$##$&\hfil${}##{}$&$##$\quad\hfil&##\hfil\cr +\fi +} +\def\endsyntax{\cr\egroup\egroup\par\syntaxvspace\noindent\ignorespaces} + +\def\firstsyntaxclass#1{ +\omit\hbox to 0pt{#1\hss}\cr +\global\let\syntaxclass=\nextsyntaxclass +} + +\def\nextsyntaxclass#1{ +\cr\noalign{\smallskip\penalty-100}\omit\hbox to 0pt{#1\hss}\cr +} + +\def\syntaxleft{ +\par\syntaxvspace\goodbreak\noindent +\bgroup +\let\\=\cr +\interlinepenalty=50 % discourage page breaks in a definition +\global\let\syntaxclass=\firstsyntaxclassleft +\if@twocolumn +\halign\bgroup\hfil$##$&\hfil${}##{}$&$##$~\hfil&##\hfil\cr +\else +\halign\bgroup\hfil$##$&\hfil${}##{}$&$##$\quad\hfil&##\hfil\cr +\fi +} +\let\endsyntaxleft=\endsyntax + +\def\firstsyntaxclassleft#1{ +$\hfilneg#1\quad\hfil$ +\global\let\syntaxclass=\nextsyntaxclassleft +} + +\def\nextsyntaxclassleft#1{ +\cr\noalign{\smallskip\goodbreak}$\hfilneg#1\quad\hfil$ +} + +% To put a frame around an arbitrary amount of vertical material. +% \begin{framed} ... \end{framed} + +\def\framed{% +\setbox0=\vbox\bgroup% +\advance\hsize by -2\fboxsep\advance\hsize by -2\fboxrule} + +\def\endframed{% +\egroup\noindent\framebox[\textwidth]{\box0}} + +% A relatively good-looking "C++". It hurts. + +\def\Cplusplus{C{\tt ++}} + +% To make slides + +\def\transp{\begin{slide}{}\@ifnextchar[{\opttitle}{}} +\def\endtransp{\end{slide}} +\def\opttitle[#1]{\titletransp{#1}} +\def\titlecolor{} + +\def\titletranspadvi#1{ + \begin{center} \titlecolor \bf #1 \\[2mm] + \includegraphics[width=\textwidth,height=0.6em]{bar.jpg.eps} + \end{center} + \bigskip} +\def\titletranspplain#1{ + {\titlecolor \begin{center} \bf #1 \end{center} \medskip \hrule} + \bigskip} +\def\titletransp#1{ + \ifx\ifadvi\undefined + \titletranspplain{#1} + \else + \ifadvi{\titletranspadvi{#1}}{\titletranspplain{#1}} + \fi} +\def\centeredtransp{ + \begin{slide}{}\@ifnextchar[{\opttitle}{} + \vspace*{0pt plus 1fil} +} +\def\endcenteredtransp{\vspace*{0pt plus 1fil}\end{slide}} + +% To put two pieces of text side by side + +\newdimen{\colwidth} +\def\sidebysidegutter{5mm} +\def\sidebysidehalfgutter{2.5mm} + +\def\sidebyside{% +\begin{center}% +\colwidth=\textwidth% +\advance\colwidth by-\sidebysidegutter% +\divide\colwidth by2% +\emergencystretch=3cm% +\begin{minipage}[t]{\colwidth}\ignorespaces} + +\def\nextto{% + \end{minipage}\kern\sidebysidegutter\begin{minipage}[t]{\colwidth}\ignorespaces}% + +\def\nexttorule{% + \end{minipage}\kern\sidebysidehalfgutter\vrule\kern\sidebysidehalfgutter\begin{minipage}[t]{\colwidth}\ignorespaces}% + +\def\endsidebyside{\end{minipage}\end{center}\ignorespaces} + +% Breaking a formula in two lines (cf. The TexBook p. 196). + +\def\twolinedisplay#1#2{\displaylines{\quad#1\hfill\cr\hfill{}#2\quad\cr}} + +% To allow breaks in identifiers or such + +\def\={\discretionary{}{}{}} + +% Write a URL, allowing breaks at slashes + +%% Doesn't work in LaTeX2e +%%\def\citeurl{% +%%\bgroup% +%%\hyphenchar\nintt=`/\hyphenchar\tentt=`/% +%%\hyphenchar\elvtt=`/\hyphenchar\twltt=`/% +%%\catcode`\~=12\relax\typeseturl} + +{\catcode`\/=13\global\def/{\char47\discretionary{}{}{}}} +\def\citeurl{\bgroup\catcode`\/=13\catcode`\~=12\relax\typeseturl} +\def\typeseturl#1{\tt #1\egroup} + +% Display a PIC drawing + +\def\showgraph{\par\medskip\centerline{\raise 1em\box\graph}\medskip} + +% Ragged right paragraph boxes in tabular environment +\def\arrayragged{\let\temp=\\\raggedright\let\\=\temp} + +% Itemize with minimal vertical size (for slides) +\def\compactitemizesize{} +\def\compactitemize{% + \advance\@itemdepth\@ne + \edef\@itemitem{labelitem\romannumeral\the\@itemdepth}% + \expandafter + \list + \csname\@itemitem\endcsname + {\compactitemizesize\parsep 0pt \topsep 0pt \itemsep 0pt \partopsep 0pt}% +} +\def\endcompactitemize{\endlist} + +% Euros + +%\def\euro{{\sf C}{\tiny$\!\!\!\!\!\!^=$}} diff --git a/papers/cfrontend_new/paper.tex b/papers/cfrontend_new/paper.tex new file mode 100755 index 0000000..4293554 --- /dev/null +++ b/papers/cfrontend_new/paper.tex @@ -0,0 +1,382 @@ +\documentclass[namedreferences]{kluwer} + +\usepackage{latexsym} +%\usepackage{amsmath} pb latex +\usepackage{amssymb} +\usepackage{amsfonts} +\usepackage{mymacros} +\usepackage{infrules} +\usepackage{url} +\usepackage{mymacros} +\usepackage[usenames]{color} + +\input{macros} + +\begin{document} +\begin{article} + +\begin{opening} +\title{Formal verification of C front-end} +\subtitle{Yet another formal verification in Coq of a C front-end} +\runningtitle{C front-end} + +\author{Sandrine \surname{Blazy} \email{{S}andrine.Blazy@ensiie.fr}} +\institute{ENSIIE and INRIA} + +\author{Xavier \surname{Leroy} \email{{X}avier.Leroy@inria.fr}} +\runningauthor{S.Blazy, X.Leroy} +\institute{INRIA} + +\maketitle + +\begin{abstract} +This paper presents +\end{abstract} + +\keywords{formal semantics, formal proof, C language, C compiler} +\end{opening} + +\section{Introduction} + +\section{A formal semantics for \Clight{}} +\subsection{CIL} + +\subsection{Abstract syntax} + +The abstract syntax of \Clight{} is given in figures~\ref{fig:syntax} +and~\ref{fig:syntax2}. +In the Coq formalization, this abstract syntax is presented as +inductive data types, therefore achieving a deep embedding of \Clight{} +into Coq. + +At the level of types, \Clight{} features all the integral types of C, +along with array, pointer (including function pointers), function +types, {\tt struct} and {\tt union} types. Bit-fields in {\tt struct} +or {\tt union} are ignored. +The integral types fully specify the bit size of integers and floats, +unlike the half-specified C types {\tt int}, {\tt long}, etc. + +\sbcm{TO DO: representation of struct and union} + +Within expressions, all C operators are supported. +Side-effects stem from function calls. +All expressions and their sub-expressions are +annotated by their static types. We write $a^\tau$ for the expression +$a$ carrying type $\tau$. These types are necessary to determine the +semantics of type-dependent operators such as the overloaded +arithmetic operators. The following expressions may be in left-value +position: $\id, *a, a_1[a_2]$ and $a \dot \id$. + +\input syntax.tex + +At the level of statements, all structured control statements of C +(conditional, loops, simple {\tt switch}, {\tt break}, {\tt continue} and +{\tt return}) are supported, but not unstructured statements +(unstructured {\tt switch} and {\tt goto}). +Contrary to C, the default case is mandatory in a \Clight{} {\tt switch} statement +and it is the last branch of the {\tt switch}. +An assignment is treated as a statement (instead of an expression). +This transformation from expression into statements is performed by CIL. +Two kinds of variables are allowed: global variables and local {\tt auto} +variables declared at the beginning of a function. Block-scoped local +variables and {\tt static} variables are omitted because they are emulated by +pulling their declarations to function scope or global scope, +respectively. Consequently, there is no block statement in \Clight{}. + +A function $f$ defined in \Clight{} consists of a header (\textit{i.e.} +{\tt fn\_params(f)} the parameters of $f$ and {\tt fn\_return(f)} +the return type of $f$), a list of local variables ({\tt fn\_vars(f)}) +and a body ({\tt fn\_body(f)}) that is a statement. The functions composing +the program are either internal functions, defined within \Clight{}, or +external functions (a.k.a. system calls). An external function consists +of the internal identifier and the signature of the function. + +A program $p$ consists of a list of global variable declarations +({\tt prog\_vars(p)}), a list of function definitions ({\tt prog\_funct(p)}), +and an identifier naming the entry point of the program ({\tt prog\_main(p)}). +In a global variable declaration, the list of initial values +represents all values that need to be stored (\textit{e.g.} the +values of the cells of an array). + +\input syntax2.tex + +\subsection{Static semantics} + The type system is very coarse: we check only the typing properties + that matter for the translation to be correct. Essentially, + we need to check that the types attached to variable references + match the declaration types for those variables. + +\subsection{Dynamic semantics} + +The dynamic semantics of \Clight{} is specified using natural semantics, +also known as big-step operational semantics. + These natural semantics capture the final result of program execution, as +well as traces of calls to external functions that emit an event when applied. +The big-step semantics described in~\cite{blazy06:fm} did not observe traces. +This addition of traces leads to a significantly +stronger observational equivalence between source and machine code. + +Execution traces represent the interactions between the program and +the rest of the world (\textit{i.e.} the input-output activities of +the program); they are defined in figure~\ref{fig:trace}. +A trace is a finite list of input-output events. +Each call to an external function produces an event. +An event consists of an identifier and the actual values of the parameters of +the called function. Usually, the identifier represents the called function, +but more generally it could also represent any observable identifier. +Starting from an initial empty event (called $\E0$), events are propagated and +concatenated during program execution. + +\input trace.tex + +While the semantics of +C is not deterministic (the evaluation order for expressions is not +completely specified and compilers are free to choose between several +orders), the semantics of \Clight{} is completely deterministic and +imposes a left-to-right evaluation order, consistent with the order +implemented by our compiler. This choice simplifies greatly the +semantics compared with, for instance, Norrish's semantics for C +\cite{Norrish:phd}, which captures (at great expense) the +non-determinism allowed by the ISO C specification. Our semantics can +therefore be viewed as a refinement of (a subset of) the ISO C +semantics, or that of Norrish. + +The semantics is defined by 7 judgements (relations): +$$\begin{array}{rclr} +G, E & |- & a, M \evallvalue \loc, \tr, M' & \mbox{(expressions in l-value position)} \\ +G, E & |- & a , M \evalexpr v, \tr, M' & \mbox{(expressions in r-value position)} \\ +G, E & |- & \seq a, M \evalexpr \seq v, \tr, M' & \mbox{(list of expressions)}\\ +G, E & |- & s, M \evalstmt \out, \tr, M' & \mbox{(statements)} \\ +G, E & |- & \ls, M \evalstmt \out, \tr, M' & \mbox{(labeled statements of a switch)} \\ +G & |- & f(\seq v), M \evalfunc v, \tr, M' & \mbox{(function invocations)} \\ + & \vdash & p \evalprog v, \tr & \mbox{(programs)} +\end{array}$$ +Each judgement relates a syntactic element (expression, statement, +etc.) and an initial memory state to the result of executing this +syntactic element, as well as the final memory state at the end of +execution and also the trace of input-output events (system calls). + The various kinds of results, as well as the evaluation +environments, are defined in figure~\ref{fig:values}. + +\input values.tex + +For instance, executing an expression $a$ in l-value position results in a +memory location $\loc$ (a memory block reference and an offset within that +block), while executing an expression $a$ in r-value position results in +the value $v$ of the expression. Values range over 32-bit integers, +64-bit floats, memory locations (pointers), and an undefined value +that represents for instance the value of uninitialized variables. +The result associated with the execution of a statement $s$ is an +``outcome'' indicating how the execution terminated: either normally +by running to completion or prematurely via a {\tt break}, {\tt continue} or +{\tt return} statement. +The invocation of a function $f$ yields a value $v$, and so does the execution +of a program. + +Two evaluation environments, defined in figure~\ref{fig:values}, +appear as parameters to the judgements. The local environment $E$ maps +local variables to references of memory blocks containing the values +of these variables. These blocks are allocated at function entry and +freed at function return. The global environment $G$ maps global +variables and function names to memory references. It also maps +some references (those corresponding to function pointers) to function +definitions. + +The memory model of the semantics is described in~\cite{icfem:sb}. +A memory $M$ maps block references to block contents. +Each block represents the result of a C \texttt{malloc}, +or a stack frame, a global static variable, or a function +code-pointer. +A block content consists of the dimensions of the block (low and high bounds) +plus a mapping from byte offsets to byte-sized memory cells (\textit{i.e.} +values). + +\sbcm{TO DO: a detailler (faire une section a part?): il faut expliquer +loadval et storeval qui sont utilisees dans la semantique.} + +In the Coq specification, the 7 judgements of the dynamic semantics +are encoded as mutually-inductive predicates. Each defining case of +each predicate corresponds exactly to an inference rule in the +conventional, on-paper presentation of natural semantics. We have one +inference rule for each kind of expression and statement described in +figure~\ref{fig:syntax}. + We show most of the inference rules in figures~\ref{fig:dynsem1} +to~\ref{fig:dynsem4}. + +\input dynsem1.tex + +The first five rules of figure~\ref{fig:dynsem1} illustrate the +evaluation of an expression in l-value position. +A variable $\id$ evaluates to the location $(E(\id), 0)$. +If an expression $a$ evaluates to a pointer value $\loc$, then +the location of the dereferencing expression $(\hbox{{\tt *}}a)^\tau$ is $\loc$. + +Rule~\ref{rule:3} shows the evaluation of an array cell. +The location of an array cell $\unannot{a_1}{\tau_1} [\unannot{a_2}{\tau_2}]$ +is computed from the location of the array $\unannot{a_1}{\tau_1}$ +({\it i.e.} the location of the first cell) and the value of the index +$\unannot{a_2}{\tau_2}$ thanks to the function {\tt add}. +{\tt add} is a partial function: +it can be undefined if the types and the shapes of argument values are +incompatible (e.g. an integer addition of two pointer values). +In the Coq specification, it is a total +function returning optional values: either {\tt None} in case of failure, or +${\tt Some}(v)$, abbreviated as $\some v$, in case of success. +%More precisely, the computation succeeds only if $v_1$ and +%$v_2$ are either 2 integers, or 2 floats or a pointer value and an integer. +%The corresponding types $\tau_1$ and $\tau_2$ must also be +%compatible with these values. For instance, if $\tau_1$ is a {\tt Tarray}, +%then $\tau_2$ must be a {\tt Tint}. +The trace resulting from the evaluation of +$\unannot{a_1}{\tau_1} [\unannot{a_2}{\tau_2}]$ is the concatenation of the +traces resulting from the evaluation of $\unannot{a_1}{\tau_1}$ and +$\unannot{a_2}{\tau_2}$. + + +In a similar way, the location of an access to a {\tt struct} field +$\unannot{a}{\tau} \dot f$ is computed from the location of the {\tt struct} +$\unannot{a}{\tau}$ and an offset with that {\tt struct} (see +rule~\ref{rule:4}). +\sbcm{un peu rapide, cf. repr ?} +The location of an access to a {\tt union} field is the location of +the {\tt union} (see rule~\ref{rule:5}). + +The last four rule of figure~\ref{fig:dynsem1} illustrate the +evaluation of an expression in r-value position. +Rule~\ref{rule:6} rule shows the evaluation of a l-value expression in an +r-value context. The expression is evaluated to its location $l$, +with final memory state $M'$. The value at location $l$ in $M'$ is +fetched using the {\tt loadval} function (see +\sbcm{(faire une section a part?)} +%section~\ref{sec:mem} +) and returned. + +If the location of an expression $a$ is $\loc$, then +the value of the expression $(\hbox{{\tt \&}}a)^\tau$ is also $\loc$ +(rule~\ref{rule:7}). +Rule~\ref{rule:8} evaluates an application of a binary operator $\op$ to +expressions $\unannot{a_1}{\tau_1}$ and $\unannot{a_2}{\tau_2}$. +Both sub-expressions are evaluated in +sequence, and their values are combined with the +{\tt eval{\char95}binary{\char95}operation} function, which takes as additional +arguments the types $\tau_1$ and $\tau_2$ of the arguments, in order to resolve +overloaded and type-dependent operators. + +Rule~\ref{rule:9} evaluates a cast expression $(\tau)\unannot{a}{\tau_a}$. +The expression $\unannot{a}{\tau_a}$ is evaluated, and its +value is cast from its natural type $\tau_a$ to the expected type +$\tau$ using the partial function {\tt cast}. This function +performs appropriate conversions, truncations and sign-extensions over +integers and floats, and may fail for undefined casts. The result $v$ +of the cast is then the final result. + +The rules in figure~\ref{fig:dynsem2} are +examples of statements execution. +The execution of a {\tt skip} statement yields the {\tt Out{\char95}normal} +outcome and the empty trace. +Similarly, the execution of a {\tt break} (resp. {\tt continue}) statement +yields the {\tt Out{\char95}break} (resp. {\tt Out{\char95}continue}) +outcome and the empty trace. + +Rule~\ref{rule:12} evaluates an assignment statement. +An assignment statement $a_1^\tau \hbox{{\tt \ =\ }} a_2^{\tau'}$ evaluates +the l-value $a_1$ to a location $\loc$, then the r-value $a_2$ to a value $v$. +As implicit casts are inserted by CIL, there is no need to cast this $v$. +$v$ is stored in memory at location $\loc$, resulting in the final memory + state $M_3$. + +The execution of a sequence of two statements starts with the +execution of the first statement, thus yielding an outcome that +determines if the second statement must be executed or not +(rules~\ref{rule:15}~and~\ref{rule:16}). +Rules~\ref{rule:17}--\ref{rule:19} describe the execution of a +{\tt while} loop. Once the condition of a while loop is evaluated to a +value $v$, the execution of the loop terminates normally if $v$ is +false. If $v$ is true, then the loop body is executed, thus yielding +an outcome $\out$. If $\out$ is {\tt Out{\char95}break}, the loop terminates +normally. If $\out$ is {\tt Out{\char95}normal} or {\tt Out{\char95}continue}, +the whole loop is reexecuted in the memory state modified by the execution of the +body. +Finally, rules~\ref{rule:20}--\ref{rule:21} describe the execution of a +{\tt return} statement. + +\input dynsem2.tex + +The rules of figure~\ref{fig:dynsem3} define the execution of a call statement. +When the expression ${a_{fun}}^{\tau}$ is evaluated to a pointer value that is the +location (in the global environment $G$) of a function $f$, and when $f$ has the +same signature as ${a_{fun}}^{\tau}$, the control flow is passed to the called +function (rule~\ref{rule:25}). + +The execution of a \Clight{} function allocates the memory required +for storing the formal parameters and the local variables of the function +(rule~\ref{rule:26}). The allocation initializes local variables to the +${\tt Vundef}$ undefined value. Formal parameters are initialized to their +corresponding actual parameters. The body of $f$ is then executed, thus yielding +an outcome. The return value of the function is computed from this outcome and +from the return type of $f$. The memory allocated for executing $f$ is freed +before returning to the caller. + +A call $<\id \, \sigma>$ to an external function triggers a new event +that is the trace resulting from that call. + +\input dynsem3.tex + +The rules of figure~\ref{fig:dynsem4} define the execution of a +${\tt switch}(a) \ls$ statement. If the expression of the {\tt switch} evaluates +to $n$, then some statements of the {\tt switch} are selected and executed +(rule~\ref{rule:28}), thus yielding an outcome $\out$. If $\out$ is +{\tt Out{\char95}break}, then the {\tt switch} terminates normally +(\textit{i.e.} the {\tt outcome{\char95}switch} function updates $\out$ into +{\tt Out{\char95}normal} and leave other outcomes unchanged). + +The first selected statements that are executed are those of either the branch +labeled by $n$ or the default branch (rules~\ref{rule:30} and \ref{rule:29}), +thus yielding an outcome that determines if the following statements must be +executed or not (rules~\ref{rule:30} and \ref{rule:31}). If needed, the execution falls through to the next statements $\ls$. + +\input dynsem4.tex + +\section{Translation from \Clight{} to Csharpminor} +\subsection{Overview of Csharpminor} +The Csharpminor language is the first intermediate language of the compiler. +It is a low-level imperative language, structured like our subset of C into +expressions, statements and functions. + +As in \Clight{}, Csharpminor local variables reside in memory, and their address +can be taken. Csharpminor is entirely processor-neutral. In particular, +Csharpminor uses a standard set of operations. + +\subsection{Overview of the translation} + +\section{Proof of correctness} + +The theorem guarantees that if the source program terminates and does +not go wrong, the compiled code terminates and does not go wrong, +performs exactly the same system calls, and returns the same exit code +as the source program. +Currently, it says nothing about source programs that do not terminate (work +in progress). + +\section{Translation from \Clight{} to Csharpminor} +\subsection{Overview of Csharpminor} +The Cminor language is the second intermediate language of the compiler +and the target language of our front-end compiler. + We now give a short overview of Cminor; see \cite{xl:popl} for a more detailed +description, and \cite{xl:compcert-backend} for a complete formal +specification. + +Unlike in Csharpminor, Cminor local variables do not reside in memory, +and their address can not be taken. + +\subsection{Overview of the translation} + +\section{Quantitative results} + +\section{Conclusion} + +\bibliographystyle{unsrt} +\bibliography{blazy} + +\end{article} +\end{document}
\ No newline at end of file diff --git a/papers/cfrontend_new/syntax.etex b/papers/cfrontend_new/syntax.etex new file mode 100755 index 0000000..344ab40 --- /dev/null +++ b/papers/cfrontend_new/syntax.etex @@ -0,0 +1,52 @@ +\begin{figure} + +\begin{syntax} +\syntaxclass{Types:} +{\it signedness} & ::= & "Signed" \alt "Unsigned" \\ +{\it intsize} & ::= & "I8" \alt "I16" \alt "I32" \\ +{\it floatsize} & ::= & "F32" \alt "F64" \\ +\tau & ::= & "Tint" ({\it intsize}, {\it signedness}) \\ + & \alt & "Tfloat" ({\it floatsize}) \\ + & \alt & "Tvoid" \\ + & \alt & "Tarray" (\tau, n) \\ + & \alt & "Tpointer" (\tau) \\ +% &\alt & "Tcomp_pointer" (\id) \\ + &\alt & "Tstruct" (\id,\seq {(\id,\tau)}) \\ + &\alt & "Tunion" (\id,\seq {(\id,\tau)}) \\ + & \alt & "Tfunction" (\seq \tau, \tau) +% +\syntaxclass{Expressions annotated with types:} +a & ::= & \unannot{a}{\tau} +\syntaxclass{Unannotated expressions:} +b & ::= & \id & variable identifier\\ + & \alt & n & integer constant\\ + & \alt & f & float constant \\ + & \alt & "sizeof"(\tau) & size of a type \\ + & \alt & \op_1 ~ a & unary arithmetic operation\\ + & \alt & a_1 ~\op_2 ~ a_2 & binary arithmetic operation\\ + & \alt & \hbox{"*"} a & dereferencing \\ + & \alt & a_1 [a_2] & array indexing \\ + & \alt & a \dot \id & field access \\ + & \alt & \hbox{"&"} a & address of \\ + & \alt & (\tau) a & cast \\ + & \alt & a_1 \hbox{" && "} a_2 \alt a_1 \hbox{" || "} a_2 + & sequential boolean operations \\ + & \alt & a(\seq a) & function call \\ +% +\op_2 & ::= & \hbox{"+"} \alt \hbox{"-"} \alt \hbox{"*"} \alt \hbox{"/"} \alt \hbox{"%"} + & arithmetic operators \\ + & \alt & \hbox{"<<"} \alt \hbox{">>"} \alt + \hbox{"&"} \alt \hbox{"|"} \alt \hbox{"^"} + & bitwise operators\\ + & \alt & \hbox{"<"} \alt \hbox{"<="} \alt \hbox{">"} \alt \hbox{">="} + \alt \hbox{"=="} \alt \hbox{"!="} + & relational operators \\ +\op_1 & ::= & \hbox{"-"} \alt \hbox{"~"} \alt \hbox{"!"}& unary operators +% +\end{syntax} +\caption{Abstract syntax of Clight (types and expressions). $\seq a$ denotes 0, 1 or several + occurrences of syntactic category $a$. $\opt a$ denotes an optional + occurrence of category $a$.} +\label{fig:syntax} +\end{figure} + diff --git a/papers/cfrontend_new/syntax2.etex b/papers/cfrontend_new/syntax2.etex new file mode 100755 index 0000000..b6ec6cf --- /dev/null +++ b/papers/cfrontend_new/syntax2.etex @@ -0,0 +1,44 @@ +\begin{figure} + +\begin{syntax} +\syntaxclass{Statements:} +s & ::= & "skip" & empty statement \\ + & \alt & a & expression evaluation\\ + & \alt & a_1 = a_2 & assignment \\ + & \alt & s_1 ; s_2 & sequence \\ + & \alt & "if"(a) ~ s_1 ~ "else" ~ s_2 & conditional \\ + & \alt & "switch"(a) \ls & switch \\ + & \alt & "while"(a) ~ s & ``while'' loop \\ + & \alt & "do" ~ s ~ "while" (a) & ``do'' loop \\ + & \alt & "for"(s_1, a, s_2)~s & ``for'' loop \\ + & \alt & "break" & exit from the current loop \\ + & \alt & "continue" & next iteration of the current loop\\ + & \alt & "return"~\opt a & return from current function +% +\syntaxclass{Switch branches:} +\ls & ::= & "default" (s) & default case switch \\ + & \alt & "case" (n, s, \ls) & non default case switch + % +\syntaxclass{Functions:} +\cfn & ::= & (\ldots \id_i: \tau_i \ldots): \tau & header\\ + & & \{ \ldots \tau_j~ \id_j ; \ldots & local variables \\ + & & ~ s ~ \} & function body +% +\syntaxclass{Function signatures:} +\sig & ::= & \ldots \tau_i \ldots \tau & \\ +% +\syntaxclass{Function definitions:} +\fn & ::= & \cfn & Clight (internal) function\\ + & \alt & <\id ~ \sig> & external function (system call) +% +\syntaxclass{Whole programs:} +{\it init} & ::= & \ldots & \\ +\prog & ::= & \ldots (\id_i,{{{\it init}}_i}^*): \tau_i \ldots & global variables (names, \\ +& & &initialized data and types) \\ + & & \ldots \id_j = \fn_j \ldots & functions (names and definitions) \\ + & & \id_{main} & entry point +\end{syntax} +\caption{Abstract syntax of Clight (statements, functions and programs). } +\label{fig:syntax2} +\end{figure} + diff --git a/papers/cfrontend_new/trace.etex b/papers/cfrontend_new/trace.etex new file mode 100644 index 0000000..d02b1fe --- /dev/null +++ b/papers/cfrontend_new/trace.etex @@ -0,0 +1,19 @@ +\begin{figure} + +\begin{syntax} +\syntaxclass{Event values:} +\evv & ::= & n & integer value\\ + & \alt & f & floating-point value +% +\syntaxclass{Events:} +\ev & ::= & \id \, \evv^* \, \evv & +% +\syntaxclass{Execution traces:} +\tr & ::= & \E0 & empty trace \\ + & \alt & [\ev] & external call \\ + & \alt & \cat \tr \tr& concatenation +\end{syntax} +\caption{Execution traces} +\label{fig:trace} +\end{figure} + diff --git a/papers/cfrontend_new/values.etex b/papers/cfrontend_new/values.etex new file mode 100755 index 0000000..bdf2858 --- /dev/null +++ b/papers/cfrontend_new/values.etex @@ -0,0 +1,40 @@ +\begin{figure} + +\begin{syntax} +\syntaxclass{Values:} +\loc & ::= & (b, n) & location (byte offset $n$ in the memory block\\ + & & & referenced by $b$)\\ +v & ::= & n & integer value\\ + & \alt & f & floating-point value \\ + & \alt & \loc & pointer value\\ +% v & ::= & "Vint"(n) & integer value\\ +% & \alt & "Vfloat"(f) & floating-point value \\ +% & \alt & "Vptr"(\loc) & pointer value\\ + & \alt & "Vundef" & undefined value +% +\syntaxclass{Statement outcomes:} +\out & ::= & "Out_normal" & go to the next statement \\ + & \alt & "Out_continue" & go to the next iteration of the current loop \\ + & \alt & "Out_break" & exit from the current loop \\ + & \alt & "Out_return" & function exit \\ + & \alt & "Out_return"(v) & function exit, returning the value $v$ +% +\syntaxclass{Global environments:} +G & ::= & (id \mapsto b) & map from global variables to block references \\ + & & \times (b \mapsto \fn) & and map from function references \\ + & & & to function definitions +% +\syntaxclass{Local environments:} +E & ::= & \id \mapsto b & map from local variables to block references +% +\syntaxclass{Memories:} +{\it bounds} & ::= & \ldots & low and high bounds \\ +{\it kind} & ::= & \ldots & content map \\ +M & ::= & b \mapsto {\it bounds} \times & map from block references to block contents\\ +& & (n \mapsto {\it kind} \mapsto v) & +\end{syntax} +% +\caption{Values, outcomes, and evaluation environments} +\label{fig:values} +\end{figure} + |