Typesetting_Technical_Reports_that_Include_Z_Specifications_Usin...

### 使用LaTeX排版包含Z规范的技术报告 #### 摘要 本文档详细介绍了如何使用LaTeX来排版含有Z语言规范的技术报告。文档结构基于位于http://www.cs.msstate.edu/allen/Msuthesis(Current 9 Jan. 2003)的示例学期论文。对于使用此模板进行LaTeX排版的进一步信息，请参考该网站。本文档内容为“使用LaTeX打印Z和Object-Z文档”一文的复制，原文由澳大利亚昆士兰大学计算机科学系的Paul King编写，日期为1990年5月29日，并可在http://svrc.it.uq.edu.au/Object-Z/pages/latex.html(Current 9 Jan. 2003)获取。有时，文档内容会超出页面边界。 #### 关键词 排版、LaTeX、Z、规范、形式化方法 ### 1. 引言 本笔记介绍了一组LaTeX宏包，用于打印Z和Object-Z规范。这些宏及其文档最初基于Mike Spivey的`zed.sty`宏包和相关文档。此宏包能够为您完成以下几项任务： 1. **加载额外字体**：加载了额外的字体并定义了用于包含Z符号的字体的助记符。 2. **定义Z符号的宏**：定义了一些不在任何字体中的Z符号宏（例如`\mapsto`）。 3. **优化数学公式中的字母设置**：修复了TeX在数学公式中设置字母的方式，使多字符标识符看起来更好。 4. **提供各种类型的“带框数学”**：提供了Z和Object-Z规范中出现的各种类型的“带框数学”。 ### 2. Schema Boxes 下面的例子展示了左侧的Schema以及如何通过LaTeX命令获得右侧的输出。 ```latex BirthdayBook known : PNAME birthday : NAME ↦ DATE known = dom birthday ``` 对应的LaTeX代码为： ```latex \begin{schema}{BirthdayBook} known : \pset{NAME} \\ birthday : NAME \pfun{DATE} \ST known = \dom{birthday} \end{schema} ``` 其中命令`\ST`（读作“Such That”）与先前使用的命令`\where`相同，后者已被保留作为向上兼容性。如果您想要一个没有名称的Schema，仅在顶部有一条水平线，则可以使用`anonschema`环境代替。 您可以设置各种参数（参见第7节）来自定义盒子样式，例如： ```latex BirthdayBook known : PNAME birthday : NAME ↦ DATE known = dom birthday ``` 在文档前言部分设置参数： ```latex \left... ``` ### 3. Z和LaTeX的集成 #### 3.1 加载必要的包 为了在LaTeX文档中正确地排版Z规范，您需要加载一些特定的包。通常，这些包括但不限于： - `amsmath`：用于增强数学环境的功能。 - `amssymb`：提供额外的数学符号。 - `stmaryrd`：用于Z规范的符号，如`\mapsto`等。 - `mathabx`：提供更多的数学符号，可能对Z规范有用。 - `pifont`：提供特殊符号，例如用于Schema盒子的边框。 #### 3.2 定义Z符号 Z语言使用了许多独特的符号，这些符号在标准LaTeX中通常是不可用的。为了支持这些符号，可以定义特定的宏。例如，可以定义以下宏： - `\pset{}`：表示幂集。 - `\pfun{}`：表示部分函数。 - `\ST`：表示“such that”。 - `\dom{}`：表示域。 #### 3.3 调整数学公式的布局 由于Z规范经常涉及复杂的数学表达式，因此需要调整LaTeX中的数学公式的布局。这可以通过自定义LaTeX宏或修改LaTeX默认的行为来实现。例如，对于多字符的标识符，可以使用`\mathit{}`宏来改善它们在数学环境中的显示效果。 ### 4. Schema盒子的定制 Schema盒子是Z规范中的核心元素之一，它们用于表示系统的不同方面或组成部分。通过定义不同的环境和宏，可以在LaTeX中自定义这些Schema盒子的外观。例如，可以通过设置边框的颜色、粗细或者背景颜色等参数来改变Schema盒子的样式。 ### 5. 实现细节 #### 5.1 使用宏包 为了实现上述功能，可以创建一个名为`zed.sty`的宏包文件，该文件包含了所有必需的定义和命令。这个宏包应该被包含在LaTeX文档的前言部分： ```latex \usepackage{zed} ``` #### 5.2 示例代码 下面是使用上述宏包的一个简单示例，展示了如何在LaTeX文档中插入一个包含Z规范的Schema盒子： ```latex \documentclass{article} \usepackage{zed} \begin{document} \begin{schema}{MySchema} known : \pset{NAME} \\ birthday : NAME \pfun{DATE} \ST known = \dom{birthday} \end{schema} \end{document} ``` 通过这种方式，您可以轻松地将Z规范集成到您的技术报告中，并确保它们以专业和一致的方式呈现出来。