From b23d8a9cb9e1b6b1b041a12872d4f62c7eda00cf Mon Sep 17 00:00:00 2001 From: Roman-Manevich Date: Fri, 17 Jul 2026 15:56:11 +0100 Subject: [PATCH 1/2] [asl reference] use \ChapterOutline to automatically list sections for a given chapter --- asllib/doc/ASLFormal.tex | 49 ++++--- asllib/doc/ASLmacros.tex | 153 ++++++++++++++++++++-- asllib/doc/AbstractSyntax.tex | 98 ++++++-------- asllib/doc/AssignableExpressions.tex | 51 ++++---- asllib/doc/BaseValues.tex | 5 +- asllib/doc/Bitfields.tex | 21 +-- asllib/doc/BlockStatements.tex | 11 +- asllib/doc/CatchingExceptions.tex | 17 +-- asllib/doc/ErrorCodes.tex | 29 ++-- asllib/doc/Expressions.tex | 82 ++++++------ asllib/doc/GlobalPragmas.tex | 15 +-- asllib/doc/GlobalStorageDeclarations.tex | 26 ++-- asllib/doc/LexicalStructure.tex | 51 ++++---- asllib/doc/Literals.tex | 17 +-- asllib/doc/LocalStorageDeclarations.tex | 27 ++-- asllib/doc/PatternMatching.tex | 33 +++-- asllib/doc/PrimitiveOperations.tex | 32 ++--- asllib/doc/RelationsOnTypes.tex | 5 +- asllib/doc/Semantics.tex | 30 ++--- asllib/doc/SideEffects.tex | 22 ++-- asllib/doc/Slicing.tex | 32 ++--- asllib/doc/Specifications.tex | 42 +++--- asllib/doc/Statements.tex | 78 ++++++----- asllib/doc/SubprogramCalls.tex | 19 +-- asllib/doc/SubprogramDeclarations.tex | 18 +-- asllib/doc/SymbolicEquivalenceTesting.tex | 14 +- asllib/doc/SymbolicSubsumptionTesting.tex | 13 +- asllib/doc/Syntax.tex | 37 +++--- asllib/doc/TopLevel.tex | 22 ++-- asllib/doc/TypeAttributes.tex | 3 +- asllib/doc/TypeChecking.tex | 10 +- asllib/doc/TypeDeclarations.tex | 14 +- asllib/doc/TypeDomains.tex | 3 +- asllib/doc/TypeSystemUtilities.tex | 1 - asllib/doc/Types.tex | 74 +++++------ asllib/doc/dictionary.txt | 2 + asllib/doc/doclint.py | 3 + asllib/doc/macros.hva | 69 ++++++++++ 38 files changed, 639 insertions(+), 589 deletions(-) diff --git a/asllib/doc/ASLFormal.tex b/asllib/doc/ASLFormal.tex index c084a95a6c..fbc2fe1dcb 100644 --- a/asllib/doc/ASLFormal.tex +++ b/asllib/doc/ASLFormal.tex @@ -4,22 +4,9 @@ \chapter{Formal System \label{chap:FormalSystem}} reference. \ChapterOutline -\begin{itemize} - \item \secref{Mathematical Definitions and Notations} defines general mathematical concepts and notations; - \item \secref{Inference Rules} defines the concept of \emph{inference rules}; - \item \secref{Transition Judgements} explains how \emph{transition judgements} can be used to represent - relations and functions; - \item \secref{Configurations} introduces \emph{\configurationsterm{}} as a way of representing compound data; - \item \secref{FlavoursOfEqualityInRules} explains the kinds of equality notations that are used to - convey intention in inference rules; - \item \secref{ASTNotations} introduces AST-related notations that are used in inference rules; - \item \secref{How to Parse Inference Rules Efficiently} explains how to efficiently parse inference rules, - \item \secref{ShortCircuitRuleMacros} defines rule macros, which compactly represent multiple rules; - \item \secref{ConventionallyUsedJudgments} presents commonly used judgements and notations; and - \item \secref{Rule Naming} explains the naming scheme for inference rules used in this reference. -\end{itemize} -\section{Mathematical Definitions and Notations\label{sec:Mathematical Definitions and Notations}} +\SectionDef[defines general mathematical concepts and notations;] + {Mathematical Definitions and Notations}{Mathematical Definitions and Notations} \hypertarget{def-triangleq}{} We use $\triangleq$ to define mathematical concepts. @@ -514,7 +501,8 @@ \subsection{OCaml-style Notations} \end{definition} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Inference Rules\label{sec:Inference Rules}} +\SectionDef[defines the concept of \emph{inference rules};] + {Inference Rules}{Inference Rules} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \hypertarget{def-inferencerule}{} An \emph{\inferencerule} (rule, for short) is an implication between a list of judgements, @@ -654,8 +642,9 @@ \section{Inference Rules\label{sec:Inference Rules}} (see \secref{Semantics of Diverging Specifications}). \end{definition} -\section{Transition Judgements\label{sec:Transition Judgements}} - +\SectionDef[explains how \emph{transition judgements} can be used to represent + relations and functions;] + {Transition Judgements}{Transition Judgements} We use rules as a structured way for defining relations (and therefore functions, as a special case). To define a relation $R \subseteq X \cartimes Y$, we use judgements of the form $\termx \rulearrow \termy$ @@ -681,8 +670,8 @@ \section{Transition Judgements\label{sec:Transition Judgements}} for a given transition. \hypertarget{def-configuration}{} -\section{Configurations\label{sec:Configurations}} - +\SectionDef[introduces \emph{\configurationsterm{}} as a way of representing compound data;] + {Configurations}{Configurations} Our relations range over compound values. That is, values that often nest tuples and lists inside other tuples and lists. We refer to such values as \emph{\configurationsterm}. To make it easier to distinguish between different \configurationsterm{}, we will sometimes attach labels to tuples using the OCaml-style notation discussed earlier. @@ -721,7 +710,9 @@ \section{Configurations\label{sec:Configurations}} Since the rule does not need to refer to the value, we do not name it and use an ignore variable instead. -\section{Flavours of Equality In Rules\label{sec:FlavoursOfEqualityInRules}} +\SectionDef[explains the kinds of equality notations that are used to + convey intention in inference rules;] + {FlavoursOfEqualityInRules}{Flavours of Equality In Rules} This section explains the equality notations used in rules, two of which are used in \SemanticsRuleRef{ECond}, shown here: \begin{mathpar} @@ -794,8 +785,8 @@ \section{Flavours of Equality In Rules\label{sec:FlavoursOfEqualityInRules}} \end{mathpar} \end{description} -\section{AST-related Notations\label{sec:ASTNotations}} - +\SectionDef[introduces AST-related notations that are used in inference rules;] + {ASTNotations}{AST-related Notations} When deconstructing AST record nodes such as $\{f_1:t_1,\ldots,f_k:t_k\}$, we sometimes only care about a subset of the fields $\{f_{i_1},\ldots,f_{i_m}\} \subset \{f_{1..k}\}$. In such cases, we write $\{f_{i_1}:t_{i_1},\ldots,f_{i_m}:t_{i_m},\ldots\}$, @@ -813,7 +804,8 @@ \section{AST-related Notations\label{sec:ASTNotations}} The partial function $\astlabel$ returns the label $\vl\in\ASTLabels$ of an AST node, when it exists. For example, $\astlabel(\TBool) = \TBool$ and $\astlabel(\TNamed(\vx)) = \TNamed$. -\section{How to Parse Inference Rules Efficiently\label{sec:How to Parse Inference Rules Efficiently}} +\SectionDef[explains how to efficiently parse inference rules,] + {How to Parse Inference Rules Efficiently}{How to Parse Inference Rules Efficiently} Consider the following examples, which is a simplified version of \SemanticsRuleRef{Binop} \begin{mathpar} \inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\\\\ @@ -858,7 +850,8 @@ \section{How to Parse Inference Rules Efficiently\label{sec:How to Parse Inferen which are components of the previously assigned variables $\vmone$ and $\vmtwo$. \hypertarget{def-shortcircuitrulemacro}{} -\section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}} +\SectionDef[defines rule macros, which compactly represent multiple rules;] + {ShortCircuitRuleMacros}{Short-circuit Rule Macros} \emph{\Shortcircuitrulemacros}, or \emph{rule macros}, for short, allow us to succinctly define sets of rules. Specifically, they allow us to capture situations where transitions have two alternative output \configurationsterm{}. @@ -1066,7 +1059,8 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}} All these cases are succinctly encoded in a single rule with the alternative output \configurationsterm{}. -\section{Conventionally-used Judgements and Notations\label{sec:ConventionallyUsedJudgments}} +\SectionDef[presents commonly used judgements and notations; and] + {ConventionallyUsedJudgments}{Conventionally-used Judgements and Notations} We now present functions used conventionally in this reference. \subsection{Checked Transitions\label{sec:Checked Transitions}} @@ -1157,7 +1151,8 @@ \subsection{Conventional Notations} \hypertarget{def-wrapline}{} The notation $\wrappedline$ denotes that a line that is longer than the page width continues on the next line. -\section{Rule Naming\label{sec:Rule Naming}} +\SectionDef[explains the naming scheme for inference rules used in this reference.] + {Rule Naming}{Rule Naming} To name a rule, we place it in a section with its name. However, some relations are defined by a group of rules. In such cases, we refer to the individual rules in a group as \emph{case rules}, diff --git a/asllib/doc/ASLmacros.tex b/asllib/doc/ASLmacros.tex index e2cc4eb515..7e024ba61d 100644 --- a/asllib/doc/ASLmacros.tex +++ b/asllib/doc/ASLmacros.tex @@ -169,16 +169,15 @@ % Not imported here means, it is not yet considered for auto-generation. \newcommand\NotImportedToASLSpecYet[1]{#1} -\newcommand\ChapterOutline[0]{\paragraph{Outline} The rest of this chapter is organized as follows:} -\newcommand\FormalRelationsDef[1]{\section{Formal Relations for #1\label{sec:Formal Relations for #1}}} -\newcommand\FormalRelationsRef[1]{\secref{Formal Relations for #1}} -\newcommand\SyntaxDef[1]{\section{Syntax of #1\label{sec:Syntax of #1}}} +\newcommand\FormalRelationsDef[2][]{\SectionDef[#1]{Formal Relations for #2}{Formal Relations for #2}} +\newcommand\FormalRelationsRef[1]{\secref{Formal Relations for #1}} % DO NOT LINT: public convenience macro. +\newcommand\SyntaxDef[2][]{\SectionDef[#1]{Syntax of #2}{Syntax of #2}} \newcommand\SyntaxRef[1]{\secref{Syntax of #1}} -\newcommand\AbstractSyntaxDef[1]{\section{Abstract Syntax of #1\label{sec:Abstract Syntax of #1}}} +\newcommand\AbstractSyntaxDef[2][]{\SectionDef[#1]{Abstract Syntax of #2}{Abstract Syntax of #2}} \newcommand\AbstractSyntaxRef[1]{\secref{Abstract Syntax of #1}} -\newcommand\TypeRulesDef[1]{\section{Type Rules for #1\label{sec:Type Rules for #1}}} -\newcommand\TypeRulesRef[1]{\secref{Type Rules for #1}} -\newcommand\SemanticsRulesDef[1]{\section{Dynamic Semantics Rules for #1\label{sec:Dynamic Semantics Rules for #1}}} +\newcommand\TypeRulesDef[2][]{\SectionDef[#1]{Type Rules for #2}{Type Rules for #2}} +\newcommand\TypeRulesRef[1]{\secref{Type Rules for #1}} % DO NOT LINT: public convenience macro. +\newcommand\SemanticsRulesDef[2][]{\SectionDef[#1]{Dynamic Semantics Rules for #2}{Dynamic Semantics Rules for #2}} \newcommand\SemanticsRulesRef[1]{\secref{Dynamic Semantics Rules for #1}} \newcommand\textfunc[1]{\textit{#1}} \newcommand\textastlabel[1]{\textsc{#1}} @@ -296,6 +295,144 @@ }% \fi } + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Chapter outline generation macros +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Use \ChapterOutline once in a chapter, after its introductory text and before +% its first section. It prints an itemized list of every \SectionDef in that +% chapter. Chapter membership is independent of file boundaries, so a chapter +% and its sections may span multiple input files. +% +% Define an outlined section as follows: +% +% \SectionDef[defines the relevant concepts;]{StableLabel}{Displayed Title} +% +% The optional first argument is the text printed after the section reference +% in the outline. It should include its final punctuation. The second +% argument is a stable label key: the section receives the label +% `sec:StableLabel' and can be referenced with \secref{StableLabel}. The third +% argument is the displayed section title. Keep the label stable when changing +% either the title or its outline description. +% +% \FormalRelationsDef, \SyntaxDef, \AbstractSyntaxDef, \TypeRulesDef, and +% \SemanticsRulesDef are convenience forms of \SectionDef. They accept the +% same optional outline description before their existing required argument. +% +% Most subsections should continue to use \subsection and do not appear in the +% chapter outline. To include a selected subsection, use: +% +% \OutlineSubsectionDef[defines a special case;]{StableLabel}{Displayed Title} +% +% It is nested under the most recent \SectionDef in the same chapter, so it must +% follow its intended parent section. +% +% Outlines are read from the previous LaTeX run, like the table of contents, so +% run LaTeX twice after changing their structure or descriptions. Their +% auxiliary data and state are separate from the rule-list macros. +\let\ASLCurrentOutlineSection\@empty +\let\ASLCurrentOutlineSectionChapter\@empty + +\newcommand\ASLChapterOutlineSection[3]{% + \item \secref{#2}% + \def\ASLChapterOutlineDescription{#3}% + \ifx\ASLChapterOutlineDescription\@empty + \else + \space #3% + \fi + \@ifundefined{ASLChapterOutlineSubsections@#1@#2}{}{% + \begin{itemize}% + \csname ASLChapterOutlineSubsections@#1@#2\endcsname + \end{itemize}% + }% +} + +\newcommand\ASLChapterOutlineEntry[3]{% + \@ifundefined{ASLChapterOutlineSeen@#1@#2}{% + \expandafter\gdef\csname ASLChapterOutlineSeen@#1@#2\endcsname{}% + \@ifundefined{ASLChapterOutline@#1}{% + \expandafter\gdef\csname ASLChapterOutline@#1\endcsname{}% + }{}% + \expandafter\g@addto@macro\csname ASLChapterOutline@#1\endcsname{% + \ASLChapterOutlineSection{#1}{#2}{#3}% + }% + }{}% +} + +\newcommand\ASLChapterOutlineSubentry[4]{% + \@ifundefined{ASLChapterOutlineSubsectionSeen@#1@#2@#3}{% + \expandafter\gdef\csname ASLChapterOutlineSubsectionSeen@#1@#2@#3\endcsname{}% + \@ifundefined{ASLChapterOutlineSubsections@#1@#2}{% + \expandafter\gdef\csname ASLChapterOutlineSubsections@#1@#2\endcsname{}% + }{}% + \expandafter\g@addto@macro\csname ASLChapterOutlineSubsections@#1@#2\endcsname{% + \item \secref{#3}% + \def\ASLChapterOutlineDescription{#4}% + \ifx\ASLChapterOutlineDescription\@empty + \else + \space #4% + \fi + }% + }{}% +} + +\newcommand\ASLPrintChapterOutline{% + \begin{itemize}% + \@ifundefined{ASLChapterOutline@\number\c@chapter}{% + \item \emph{Run LaTeX again to generate this chapter outline.}% + }{% + \csname ASLChapterOutline@\number\c@chapter\endcsname + }% + \end{itemize}% +} + +\newcommand\ChapterOutline[0]{% + \@ifundefined{ASLChapterOutlinePrinted@\number\c@chapter}{% + \expandafter\gdef\csname ASLChapterOutlinePrinted@\number\c@chapter\endcsname{}% + }{% + \PackageError{ASLReference}{Multiple chapter outlines in chapter \number\c@chapter}{}% + }% + \global\let\ASLCurrentOutlineSection\@empty + \global\let\ASLCurrentOutlineSectionChapter\@empty + \paragraph{Outline} The rest of this chapter is organized as follows: + \ASLPrintChapterOutline +} + +\newcommand\SectionDef[3][]{% + \section{#3\label{sec:#2}}% + \@ifundefined{ASLChapterOutlineWritten@\number\c@chapter @#2}{% + \expandafter\gdef\csname ASLChapterOutlineWritten@\number\c@chapter @#2\endcsname{}% + }{% + \PackageError{ASLReference}{Duplicate outline section `#2' in chapter \number\c@chapter}{}% + }% + \xdef\ASLCurrentOutlineSectionChapter{\number\c@chapter}% + \gdef\ASLCurrentOutlineSection{#2}% + \immediate\write\@auxout{% + \string\ASLChapterOutlineEntry{\number\c@chapter}{\unexpanded{#2}}{\unexpanded{#1}}% + }% +} + +\newcommand\OutlineSubsectionDef[3][]{% + \subsection{#3\label{sec:#2}}% + \@ifundefined{ASLChapterOutlineSubsectionWritten@\number\c@chapter @#2}{% + \expandafter\gdef\csname ASLChapterOutlineSubsectionWritten@\number\c@chapter @#2\endcsname{}% + }{% + \PackageError{ASLReference}{Duplicate outline subsection `#2' in chapter \number\c@chapter}{}% + }% + \edef\ASLCurrentChapter{\number\c@chapter}% + \ifx\ASLCurrentOutlineSection\@empty + \PackageError{ASLReference}{Outline subsection `#2' has no preceding outline section}{}% + \else + \ifx\ASLCurrentChapter\ASLCurrentOutlineSectionChapter + \immediate\write\@auxout{% + \string\ASLChapterOutlineSubentry{\number\c@chapter}{\expandafter\unexpanded\expandafter{\ASLCurrentOutlineSection}}{\unexpanded{#2}}{\unexpanded{#1}}% + }% + \else + \PackageError{ASLReference}{Outline subsection `#2' has no preceding outline section in this chapter}{}% + \fi + \fi +} \makeatother %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/asllib/doc/AbstractSyntax.tex b/asllib/doc/AbstractSyntax.tex index 9ce5f4bd45..6f518ebf4a 100644 --- a/asllib/doc/AbstractSyntax.tex +++ b/asllib/doc/AbstractSyntax.tex @@ -27,39 +27,9 @@ \chapter{Abstract Syntax\label{chap:AbstractSyntax}} generate a \typedast. \ChapterOutline -\begin{itemize} - \item \secref{AbstractSyntaxTrees} defines the type of Abstract Syntax Trees (ASTs) used by ASL; - \item \secref{AbstractSyntaxGrammar} defines notations used to define the ASTs of ASL; - \item \secref{UntypedAbstractGrammar} defines the AST nodes for the \untypedast: - \begin{itemize} - \item \secref{Identifiers} defines the AST for identifiers; - \item \secref{ASTLiterals} defines the AST for literal values; - \item \secref{Operators} defines the AST for operators; - \item \secref{Expressions} defines the AST for expressions; - \item \secref{Patterns} defines the AST for patterns; - \item \secref{Slices} defines the AST for slices; - \item \secref{SubprogramCalls} defines the AST for subprogram calls; - \item \secref{Types} defines the AST for types; - \item \secref{Constraints} defines the AST for constraints; - \item \secref{BitFields} defines the AST for bitfields; - \item \secref{FieldsAndTypedIdentifiers} defines the AST for fields and typed identifiers; - \item \secref{AssignableExpressions} defines the AST for assignable expressions; - \item \secref{LocalDeclarations} defines the AST for local declarations; - \item \secref{Statements} defines the AST for statements; - \item \secref{CaseAlternatives} defines the AST for case alternatives; - \item \secref{ExceptionCatchers} defines the AST for exception catchers; - \item \secref{Subprograms} defines the AST for subprograms; - \item \secref{GlobalDeclarations} defines the AST for global declarations; - \item \secref{Specifications} defines the AST for specifications; - \end{itemize} - \item \secref{TypedAbstractSyntax} defines the \typedast; - \item \secref{BuildingAbstractSyntaxTrees} explains how we use inference rules to transform a parse tree into an \untypedast; - \item \secref{BuildingParameterisedProductions} presents rules for building ASTs from parameterised productions; - \item \secref{LeftToRight} maps \assignableexpressions{} to right-hand side expressions; - \item \secref{AbstractSyntaxAbbreviations} defines AST abbreviations used by inference rules throughout this reference. -\end{itemize} -\section{Abstract Syntax Trees\label{sec:AbstractSyntaxTrees}} +\SectionDef[defines the type of Abstract Syntax Trees (ASTs) used by ASL;] + {AbstractSyntaxTrees}{Abstract Syntax Trees} In an ASL abstract syntax tree, a node is one of the following data types: \begin{description} @@ -79,7 +49,8 @@ \section{Abstract Syntax Trees\label{sec:AbstractSyntaxTrees}} The function $\substrecordfield(r, f, n)$ takes a record AST node $r$, a field name $f$ and an AST node $n$ and returns an AST record node $r'$ where the $f$ field is bound to $n$. -\section{Abstract Syntax Grammar\label{sec:AbstractSyntaxGrammar}} +\SectionDef[defines notations used to define the ASTs of ASL;] + {AbstractSyntaxGrammar}{Abstract Syntax Grammar} An abstract syntax is defined in terms of derivation rules containing variables (also referred to as non-terminals). % @@ -99,23 +70,24 @@ \section{Abstract Syntax Grammar\label{sec:AbstractSyntaxGrammar}} An abstract syntax consists of a set of derivation rules and a start non-terminal. -\section{Untyped Abstract Grammar\label{sec:UntypedAbstractGrammar}} +\SectionDef[defines the AST nodes for the \untypedast:] + {UntypedAbstractGrammar}{Untyped Abstract Grammar} The abstract syntax of ASL is given in terms of the derivation rules below and the start non-terminal $\spec$. % Some extra details are given by using the notation $\overtext{\textit{symbol}}{\text{detail}}$. -\subsection{Identifiers \label{sec:Identifiers}} +\OutlineSubsectionDef[defines the AST for identifiers;]{Identifiers}{Identifiers} Identifiers in the AST, denoted $\Identifier$ are simply strings representing ASL identifiers. Those are obtained directly from the values of identifier tokens, $\Tidentifier(s)$. -\subsection{Literal Values \label{sec:ASTLiterals}} +\OutlineSubsectionDef[defines the AST for literal values;]{ASTLiterals}{Literal Values} The following rules correspond to literal values of the following ASL data types: integers, Booleans, real numbers, bitvectors, and strings. \RenderType{literal} -\subsection{Operators\label{sec:Operators}} +\OutlineSubsectionDef[defines the AST for operators;]{Operators}{Operators} The following rules correspond to unary operators and binary operators, which can be used in unary expressions and binary expressions. @@ -171,7 +143,7 @@ \subsection{Operators\label{sec:Operators}} \end{tabular} \end{center} -\subsection{Expressions \label{sec:Expressions}} +\OutlineSubsectionDef[defines the AST for expressions;]{Expressions}{Expressions} The following rules correspond to various types of expressions: literal expressions, variable expressions, type assertions, binary operation expressions, unary operation expressions, call expressions, slicing expressions, conditional expressions, array access expressions, single-field access expressions, multiple-field access expressions, @@ -180,29 +152,30 @@ \subsection{Expressions \label{sec:Expressions}} \RenderTypes{untyped_expr} -\subsection{Patterns \label{sec:Patterns}} +\OutlineSubsectionDef[defines the AST for patterns;]{Patterns}{Patterns} \hypertarget{constant-zerobit}{} \hypertarget{constant-onebit}{} \hypertarget{constant-xbit}{} \RenderType{pattern} -\subsection{Slices \label{sec:Slices}} +\OutlineSubsectionDef[defines the AST for slices;]{Slices}{Slices} \RenderTypes{untyped_slice} -\subsection{Subprogram calls \label{sec:SubprogramCalls}} +\OutlineSubsectionDef[defines the AST for subprogram calls;]{SubprogramCalls}{Subprogram calls} \RenderType{call} -\subsection{Types \label{sec:Types}} +\OutlineSubsectionDef[defines the AST for types;]{Types}{Types} \RenderType{ty} -\subsection{Constraints \label{sec:Constraints}} +\OutlineSubsectionDef[defines the AST for constraints;]{Constraints}{Constraints} \RenderTypes{untyped_constraint_kind} \RenderType{int_constraint} -\subsection{Bit Fields \label{sec:BitFields}} +\OutlineSubsectionDef[defines the AST for bitfields;]{BitFields}{Bit Fields} \RenderType{bitfield} -\subsection{Fields and Typed Identifiers \label{sec:FieldsAndTypedIdentifiers}} +\OutlineSubsectionDef[defines the AST for fields and typed identifiers;] + {FieldsAndTypedIdentifiers}{Fields and Typed Identifiers} The following rule corresponds to a field of a record-like structure: \RenderType{field} @@ -210,11 +183,13 @@ \subsection{Fields and Typed Identifiers \label{sec:FieldsAndTypedIdentifiers}} The following rule corresponds to an identifier with its associated type: \RenderType{typed_identifier} -\subsection{Assignable Expressions \label{sec:AssignableExpressions}} +\OutlineSubsectionDef[defines the AST for assignable expressions;] + {AssignableExpressions}{Assignable Expressions} The following rules define the types of left-hand side of assignments: \RenderTypes{untyped_lexpr} -\subsection{Local Declarations \label{sec:LocalDeclarations}} +\OutlineSubsectionDef[defines the AST for local declarations;] + {LocalDeclarations}{Local Declarations} A local declaration keyword specifies whether a local storage declaration is mutable or immutable: \RenderType{local_decl_keyword} @@ -230,32 +205,35 @@ \subsection{Local Declarations \label{sec:LocalDeclarations}} \RenderType{local_decl_item} -\subsection{Statements \label{sec:Statements}} +\OutlineSubsectionDef[defines the AST for statements;]{Statements}{Statements} \RenderTypes{untyped_stmt} \RenderType{for_direction} -\subsection{Case Alternatives \label{sec:CaseAlternatives}} +\OutlineSubsectionDef[defines the AST for case alternatives;] + {CaseAlternatives}{Case Alternatives} \RenderType{case_alt} -\subsection{Exception Catchers \label{sec:ExceptionCatchers}} +\OutlineSubsectionDef[defines the AST for exception catchers;] + {ExceptionCatchers}{Exception Catchers} \RenderType{catcher} -\subsection{Subprograms \label{sec:Subprograms}} +\OutlineSubsectionDef[defines the AST for subprograms;]{Subprograms}{Subprograms} \RenderType{subprogram_type} \RenderType{func_qualifier} \RenderType{override_info} \RenderType{func} -\subsection{Global Declarations \label{sec:GlobalDeclarations}} +\OutlineSubsectionDef[defines the AST for global declarations;] + {GlobalDeclarations}{Global Declarations} Declaration keyword for global storage elements: \RenderType{global_decl_keyword} \RenderType{global_decl} \RenderType{decl} -\subsection{Specifications \label{sec:Specifications}} +\OutlineSubsectionDef[defines the AST for specifications;]{Specifications}{Specifications} \RenderType{spec} -\section{Typed Abstract Syntax\label{sec:TypedAbstractSyntax}} +\SectionDef[defines the \typedast;]{TypedAbstractSyntax}{Typed Abstract Syntax} The derivation rules for the typed abstract syntax are the same as the rules for the untyped abstract syntax, except for the following differences. @@ -310,7 +288,8 @@ \section{Typed Abstract Syntax\label{sec:TypedAbstractSyntax}} Global pragma declarations $\DPragma$ are removed from the \untypedast\ once their expressions have been typechecked and do not appear in the \typedast. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Building Abstract Syntax Trees\label{sec:BuildingAbstractSyntaxTrees}} +\SectionDef[explains how we use inference rules to transform a parse tree into an \untypedast;] + {BuildingAbstractSyntaxTrees}{Building Abstract Syntax Trees} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% This section defines how to transform a parse tree into the corresponding AST via recursively traversing the parse tree and applying a \emph{builder} function @@ -403,7 +382,8 @@ \subsection{Abbreviated Rule Notation for AST Builders} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Building Parameterised Productions\label{sec:BuildingParameterisedProductions}} +\SectionDef[presents rules for building ASTs from parameterised productions;] + {BuildingParameterisedProductions}{Building Parameterised Productions} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% This section defines builder relations for the subset of macro productions in \secref{ParametricProductions} @@ -570,7 +550,8 @@ \section{Building Parameterised Productions\label{sec:BuildingParameterisedProdu \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Transforming Assignable Expressions\label{sec:LeftToRight}} +\SectionDef[maps \assignableexpressions{} to right-hand side expressions;] + {LeftToRight}{Transforming Assignable Expressions} \RenderRelation{rexpr} This function is utilised by both the type system and the dynamic semantics. @@ -578,7 +559,8 @@ \section{Transforming Assignable Expressions\label{sec:LeftToRight}} \RenderProseAndFormally{rexpr} -\section{Abstract Syntax Abbreviations\label{sec:AbstractSyntaxAbbreviations}} +\SectionDef[defines AST abbreviations used by inference rules throughout this reference.] + {AbstractSyntaxAbbreviations}{Abstract Syntax Abbreviations} We employ the following abbreviations for various AST nodes: \begin{center} \begin{tabular}{ll} diff --git a/asllib/doc/AssignableExpressions.tex b/asllib/doc/AssignableExpressions.tex index 645e230cd7..cddf5babeb 100644 --- a/asllib/doc/AssignableExpressions.tex +++ b/asllib/doc/AssignableExpressions.tex @@ -13,25 +13,10 @@ \chapter{Assignable Expressions\label{chap:AssignableExpressions}} to satisfy \\ \SyntacticSugarRef{SetterFieldAssignment}. \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Assignable Expressions} introduces the formal relations for - \assignableexpressions; - \item \SyntaxRef{Assignable Expressions} defines the syntax for \assignableexpressions; - \item \AbstractSyntaxRef{Assignable Expressions} defines the functions needed to build - the AST for \assignableexpressions{}. These make use of desugaring functions, - defined in \secref{AssignableExpressionsDesugaring}; - \item \secref{DiscardingAssignmentExpressions} defines discarding assignment expressions; - \item \secref{VariableAssignmentExpressions} defines variable assignment expressions; - \item \secref{MultiAssignmentExpressions} defines multi-assignment expressions; - \item \secref{ArrayAssignmentExpressions} defines array assignment expressions; - \item \secref{BitvectorSliceAssignmentExpressions} defines bitvector slice assignment expressions; - \item \secref{StructuredTypeFieldAssignmentExpressions} defines structured type field assignment expressions; - \item \secref{StructuredTypeMultiFieldAssignmentExpressions} defines structured type multi-field assignment expressions; - \item \secref{BitfieldAssignableExpressions} defines bitfield assignment expressions. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Assignable Expressions} +\FormalRelationsDef[introduces the formal relations for + \assignableexpressions;]{Assignable Expressions} \paragraph{Syntax:} Assignable expressions are grammatically derived from $\Nlexpr$. \paragraph{Abstract Syntax:} Assignable expressions are derived in the abstract syntax from $\lexpr$ @@ -57,7 +42,7 @@ \chapter{Assignable Expressions\label{chap:AssignableExpressions}} using $\texttt{eval\_expr}$ to evaluate it. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef{Assignable Expressions} +\SyntaxDef[defines the syntax for \assignableexpressions;]{Assignable Expressions} \begin{flalign*} \Nlexpr \derives\ & \Tminus &\\ @@ -97,8 +82,9 @@ \chapter{Assignable Expressions\label{chap:AssignableExpressions}} It is \desugared{} by \ASTRuleRef{DesugarLHSFieldsTuple}. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Assignable Expressions} - +\AbstractSyntaxDef[defines the functions needed to build + the AST for \assignableexpressions{}. These make use of desugaring functions, + defined in \secref{AssignableExpressionsDesugaring};]{Assignable Expressions} We first define $\lhsaccess$, which we use in this section as an intermediate representation between some syntax forms of \assignableexpressions{} and their corresponding abstract syntax. In particular, rather than directly building the abstract syntax for these \assignableexpressions{}, @@ -453,7 +439,8 @@ \subsection{Desugaring Assignable Expressions\label{sec:AssignableExpressionsDes \end{mathpar} \hypertarget{def-discardlexprterm}{} -\section{Discarding Assignment Expressions\label{sec:DiscardingAssignmentExpressions}} +\SectionDef[defines discarding assignment expressions;] + {DiscardingAssignmentExpressions}{Discarding Assignment Expressions} \subsection{Abstract Syntax} \RenderTypes[remove_hypertargets]{lexpr_discard} @@ -479,7 +466,8 @@ \subsection{Semantics} \CodeSubsection{\EvalLEDiscardBegin}{\EvalLEDiscardEnd}{../Interpreter.ml} \hypertarget{def-varlexprterm}{} -\section{Variable Assignment Expressions\label{sec:VariableAssignmentExpressions}} +\SectionDef[defines variable assignment expressions;] + {VariableAssignmentExpressions}{Variable Assignment Expressions} \subsection{Abstract Syntax} \RenderTypes[remove_hypertargets]{lexpr_var} @@ -519,7 +507,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_lexpr_LEVar} \CodeSubsection{\EvalLEVarBegin}{\EvalLEVarEnd}{../Interpreter.ml} -\section{Multi-assignment Expressions\label{sec:MultiAssignmentExpressions}} +\SectionDef[defines multi-assignment expressions;] + {MultiAssignmentExpressions}{Multi-assignment Expressions} \hypertarget{def-destructuringlexprterm}{} \ASLListing{Assignment to multiple left-hand-side expressions}{semantics-ledestructuring}{\semanticstests/SemanticsRule.LEDestructuring.asl} @@ -594,7 +583,8 @@ \subsection{Semantics} \RenderRule{protected_multi_assign} \hypertarget{def-setarraylexprterm}{} -\section{Array Assignment Expressions\label{sec:ArrayAssignmentExpressions}} +\SectionDef[defines array assignment expressions;] + {ArrayAssignmentExpressions}{Array Assignment Expressions} This section details the syntax, abstract syntax, semantics, and typing of array write expressions. \subsection{Abstract Syntax} @@ -633,7 +623,8 @@ \subsubsection{Comments} See \SyntacticSugarRef{SetterFieldAssignment}. \hypertarget{def-slicelexprterm}{} -\section{Bitvector Slice Assignment Expressions\label{sec:BitvectorSliceAssignmentExpressions}} +\SectionDef[defines bitvector slice assignment expressions;] + {BitvectorSliceAssignmentExpressions}{Bitvector Slice Assignment Expressions} \ASLListing{Assignable slice expressions}{semantics-leslice}{\semanticstests/SemanticsRule.LESlice.asl} \subsection{Abstract Syntax} @@ -699,7 +690,8 @@ \subsubsection{Comments} \RenderProseAndFormally{check_two_ranges_non_overlapping} \hypertarget{def-setfieldlexprterm}{} -\section{Structured Type Field Assignment Expressions\label{sec:StructuredTypeFieldAssignmentExpressions}} +\SectionDef[defines structured type field assignment expressions;] + {StructuredTypeFieldAssignmentExpressions}{Structured Type Field Assignment Expressions} \subsection{Abstract Syntax} \RenderTypes[remove_hypertargets]{lexpr_setfield} @@ -756,8 +748,8 @@ \subsubsection{Comments} See \SyntacticSugarRef{SetterFieldAssignment}. -\section{Structured Type Multi-field Assignment Expressions\label{sec:StructuredTypeMultiFieldAssignmentExpressions}} - +\SectionDef[defines structured type multi-field assignment expressions;] + {StructuredTypeMultiFieldAssignmentExpressions}{Structured Type Multi-field Assignment Expressions} \ASLListing{Multi-field assignment expression}{lesetfields}{\typingtests/TypingRule.LESetFields.asl} \subsection{Abstract Syntax} @@ -811,7 +803,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_lexpr_LESetCollectionFields} -\section{Bitfield Assignable Expressions\label{sec:BitfieldAssignableExpressions}} +\SectionDef[defines bitfield assignment expressions.] + {BitfieldAssignableExpressions}{Bitfield Assignable Expressions} \subsection{Abstract Syntax} \RenderTypes[remove_hypertargets]{lexpr_slice} diff --git a/asllib/doc/BaseValues.tex b/asllib/doc/BaseValues.tex index 5ed05c3770..4d63a64e17 100644 --- a/asllib/doc/BaseValues.tex +++ b/asllib/doc/BaseValues.tex @@ -1,4 +1,7 @@ -\section{Base Values\label{sec:BaseValues}} +\SectionDef[defines how to generate a \emph{base value} --- an expression + to initialise a storage element of a given type for which no initialising + expression is given.] + {BaseValues}{Base Values} \hypertarget{def-basevalueterm}{} Each type, with the exceptions stated below, has a \basevalueterm, which is used to initialise storage elements (either local or global), diff --git a/asllib/doc/Bitfields.tex b/asllib/doc/Bitfields.tex index 4cec1a3332..713b8d8f83 100644 --- a/asllib/doc/Bitfields.tex +++ b/asllib/doc/Bitfields.tex @@ -26,16 +26,9 @@ \chapter{Bitfields\label{chap:Bitfields}} and a slice of the form \texttt{[$\veone$+:$\vetwo$]} as a \lengthslice. \ChapterOutline -\begin{itemize} - \item \secref{Nested Bitfields} describes nested bitfields; - \item \FormalRelationsRef{Bitfields} defines the formal relations for bitfields; - \item \SyntaxRef{Bitfields} defines the syntax of bitfields; - \item \AbstractSyntaxRef{Bitfields} defines the abstract syntax of bitfields; - \item \TypeRulesRef{Bitfields} defines the type system rules for bitfields; and - \item \SemanticsRulesRef{Bitfields} defines the dynamic semantics of bitfields. -\end{itemize} -\section{Nested Bitfields\label{sec:Nested Bitfields}} +\SectionDef[describes nested bitfields;] + {Nested Bitfields}{Nested Bitfields} Bitfields may have nested bitfields. This can have several uses, one of which is being able to define two different views of a register. @@ -94,7 +87,7 @@ \section{Nested Bitfields\label{sec:Nested Bitfields}} \ASLListing{A bitvector type with nested bitfields}{nestedbitfields}{\definitiontests/Bitfields_nested.asl} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Bitfields} +\FormalRelationsDef[defines the formal relations for bitfields;]{Bitfields} \paragraph{Syntax:} Bitfields are grammatically derived from $\Nbitfield$ and lists of bitfields are grammatically derived from $\Nbitfields$. @@ -109,7 +102,7 @@ \section{Nested Bitfields\label{sec:Nested Bitfields}} $\evallexpr$ (see \secref{BitvectorSliceAssignmentExpressions}). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef{Bitfields} +\SyntaxDef[defines the syntax of bitfields;]{Bitfields} \begin{flalign*} \Nbitfields \derives \ & \Tlbrace \parsesep \TClistZero{\Nbitfield} \parsesep \Trbrace &\\ \Nbitfield \derives \ & \Nslices \parsesep \Tidentifier &\\ @@ -118,7 +111,7 @@ \section{Nested Bitfields\label{sec:Nested Bitfields}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Bitfields} +\AbstractSyntaxDef[defines the abstract syntax of bitfields;]{Bitfields} \RenderType[remove_hypertargets]{bitfield} \ASTRuleDef{Bitfields} @@ -186,7 +179,7 @@ \section{Nested Bitfields\label{sec:Nested Bitfields}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef{Bitfields} +\TypeRulesDef[defines the type system rules for bitfields; and]{Bitfields} \TypingRuleDef{TBitFields} \RenderRelation{annotate_bitfields} @@ -402,7 +395,7 @@ \section{Nested Bitfields\label{sec:Nested Bitfields}} \RenderProseAndFormally{slice_to_indices} -\SemanticsRulesDef{Bitfields} +\SemanticsRulesDef[defines the dynamic semantics of bitfields.]{Bitfields} The type system annotates expressions that read from a bitfield into corresponding slicing \rhsexpressions{}. Therefore, reading from a bitfield is done by evaluating a corresponding slice expression (see \SemanticsRuleRef{ESlice}). diff --git a/asllib/doc/BlockStatements.tex b/asllib/doc/BlockStatements.tex index 178cb86718..c82b593619 100644 --- a/asllib/doc/BlockStatements.tex +++ b/asllib/doc/BlockStatements.tex @@ -22,14 +22,9 @@ \chapter{Block Statements\label{chap:BlockStatements}} \ASLListing{A conditional statement defining a block structure}{block}{\semanticstests/SemanticsRule.Block.asl} \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Block Statements} defines the formal relations for block statements; - \item \TypeRulesRef{Block Statements} defines the type rule for block statements; and - \item \SemanticsRulesRef{Block Statements} defines the semantics of block statements. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Block Statements} +\FormalRelationsDef[defines the formal relations for block statements;]{Block Statements} \paragraph{Syntax:} Block statements are grammatically the same as other statements derived from $\Nstmt$. @@ -41,7 +36,7 @@ \chapter{Block Statements\label{chap:BlockStatements}} \paragraph{Semantics:} Block statements are evaluated by $\evalblock$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef{Block Statements} +\TypeRulesDef[defines the type rule for block statements; and]{Block Statements} \RenderRelation{annotate_block} \TypingRuleDef{Block} @@ -57,7 +52,7 @@ \subsection{Comments} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SemanticsRulesDef{Block Statements} +\SemanticsRulesDef[defines the semantics of block statements.]{Block Statements} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RenderRelation{eval_block} diff --git a/asllib/doc/CatchingExceptions.tex b/asllib/doc/CatchingExceptions.tex index fd17750d9a..126027eddf 100644 --- a/asllib/doc/CatchingExceptions.tex +++ b/asllib/doc/CatchingExceptions.tex @@ -22,16 +22,9 @@ \chapter{Catching Exceptions\label{chap:CatchingExceptions}} \ASLListing{Catching exceptions}{CatchingExceptions2}{\definitiontests/CatchingExceptions2.asl} \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Exception Catchers} defines the formal relations for exception catchers; - \item \SyntaxRef{Exception Catchers} defines the syntax of exception catchers; - \item \AbstractSyntaxRef{Exception Catchers} defines the abstract syntax of exception catchers; - \item \TypeRulesRef{Exception Catchers} defines the type rules for exception catchers; - \item \SemanticsRulesRef{Exception Catchers} defines the dynamic semantics of exception catchers. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Exception Catchers} +\FormalRelationsDef[defines the formal relations for exception catchers;]{Exception Catchers} \paragraph{Syntax:} Exception catchers are grammatically derived from $\Ncatcher$. \paragraph{Abstract Syntax:} Exception catchers are derived in the abstract syntax by $\catcher$ and generated using $\buildcatcher$. @@ -39,14 +32,14 @@ \chapter{Catching Exceptions\label{chap:CatchingExceptions}} \paragraph{Semantics:} Exception catchers are evaluated via $\evalcatchers$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef{Exception Catchers} +\SyntaxDef[defines the syntax of exception catchers;]{Exception Catchers} \begin{flalign*} \Ncatcher \derives \ & \Twhen \parsesep \Tidentifier \parsesep \Tcolon \parsesep \Nty \parsesep \Tarrow \parsesep \Nstmtlist &\\ |\ & \Twhen \parsesep \Nty \parsesep \Tarrow \parsesep \Nstmtlist &\\ \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Exception Catchers} +\AbstractSyntaxDef[defines the abstract syntax of exception catchers;]{Exception Catchers} \RenderType[remove_hypertargets]{catcher} \ASTRuleDef{Catcher} @@ -84,7 +77,7 @@ \chapter{Catching Exceptions\label{chap:CatchingExceptions}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef{Exception Catchers} +\TypeRulesDef[defines the type rules for exception catchers;]{Exception Catchers} \RenderRelation{annotate_catcher} \TypingRuleDef{Catcher} @@ -100,7 +93,7 @@ \chapter{Catching Exceptions\label{chap:CatchingExceptions}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SemanticsRulesDef{Exception Catchers} +\SemanticsRulesDef[defines the dynamic semantics of exception catchers.]{Exception Catchers} The semantic relation for evaluating catchers employs an argument that is an output configuration. This argument corresponds to the result of evaluating a \trystatementterm{} and its type is defined as follows: diff --git a/asllib/doc/ErrorCodes.tex b/asllib/doc/ErrorCodes.tex index c250745a04..ba30750b1a 100644 --- a/asllib/doc/ErrorCodes.tex +++ b/asllib/doc/ErrorCodes.tex @@ -8,18 +8,10 @@ \chapter{Errors\label{chap:Errors}} including when these errors must be detected and reported to users. \ChapterOutline -\begin{itemize} - \item \secref{How Implementations Should Handle Errors} describes how implementations of ASL - should handle errors; - \item \secref{Error Kinds} defines a classification of ASL errors; - \item \secref{ErrorCodesSummary} summarises the error codes used throughout this reference; - \item \secref{BuildErrors} details \builderrorsterm; - \item \secref{TypingErrors} details \typingerrorsterm; - \item \secref{DynamicErrors} details \dynamicerrorsterm. -\end{itemize} - -\section{How Implementations Should Handle Errors\label{sec:How Implementations Should Handle Errors}} +\SectionDef[describes how implementations of ASL + should handle errors;] + {How Implementations Should Handle Errors}{How Implementations Should Handle Errors} \RequirementDef{StaticErrorCheck} Implementations should detect and report \staticerrorsterm. \\ Specifically, \staticerrorsterm{} must never cause a \dynamicerrorterm{} or cause an exception to be raised. @@ -104,7 +96,8 @@ \section{How Implementations Should Handle Errors\label{sec:How Implementations \end{Verbatim} % CONSOLE_END -\section{Error Kinds\label{sec:Error Kinds}} +\SectionDef[defines a classification of ASL errors;] + {Error Kinds}{Error Kinds} \hypertarget{def-errorcodeterm}{} Each type of error has an \emph{\errorcodeterm}, which uniquely identifies it (see \secref{ErrorCodesSummary} for the full list of \errorcodesterm), @@ -137,7 +130,8 @@ \section{Error Kinds\label{sec:Error Kinds}} \Builderrorsterm{} and \typingerrorsterm{} are known collectively as \staticerrorsterm. -\section{Error Codes Summary\label{sec:ErrorCodesSummary}} +\SectionDef[summarises the error codes used throughout this reference;] + {ErrorCodesSummary}{Error Codes Summary} The following table summarises all error codes. \begin{center} @@ -185,7 +179,8 @@ \section{Error Codes Summary\label{sec:ErrorCodesSummary}} \end{tabular} \end{center} -\section{Build Errors\label{sec:BuildErrors}} +\SectionDef[details \builderrorsterm;] + {BuildErrors}{Build Errors} \begin{description} \item[$\LexicalError$] \textit{Lexical error.} @@ -216,7 +211,8 @@ \section{Build Errors\label{sec:BuildErrors}} For example, the standard library defines a non-subprogram (\ASTRuleRef{SetBuiltin}). \end{description} -\section{Type Errors\label{sec:TypingErrors}} +\SectionDef[details \typingerrorsterm;] + {TypingErrors}{Type Errors} \begin{description} \hypertarget{def-undefinedidentifier}{} @@ -396,7 +392,8 @@ \section{Type Errors\label{sec:TypingErrors}} See \TypingRuleRef{LDVar}. \end{description} -\section{Dynamic Errors\label{sec:DynamicErrors}} +\SectionDef[details \dynamicerrorsterm.] + {DynamicErrors}{Dynamic Errors} \begin{description} \hypertarget{def-unreachableerror}{} diff --git a/asllib/doc/Expressions.tex b/asllib/doc/Expressions.tex index 91257f2626..c268330af4 100644 --- a/asllib/doc/Expressions.tex +++ b/asllib/doc/Expressions.tex @@ -17,31 +17,9 @@ \chapter{Expressions\label{chap:Expressions}} \ASLListing{More examples of expressions}{expr2}{\syntaxtests/expr2.asl} \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Expressions} defines the formal relations for expressions; - \item \secref{LiteralExpressions} defines \literalexpressionsterm; - \item \secref{VariableExpressions} defines \variableexpressionsterm; - \item \secref{BinaryExpressions} defines \binopexpressionsterm; - \item \secref{UnaryExpressions} defines \unopexpressionsterm; - \item \secref{ConditionalExpressions} defines \condexpressionsterm; - \item \secref{CallExpressions} defines \callexpressionsterm; - \item \secref{SlicingExpressions} defines \slicingexpressionsterm; - \item \secref{ArrayAccessExpressions} defines \arrayaccessexpressionsterm; - \item \secref{FieldReadingExpressions} defines field reading expressions; - \item \secref{MultiFieldReadingExpressions} defines multi-field reading expressions; - \item \secref{AssertingTypeConversionExpressions} defines asserting type conversion expressions; - \item \secref{PatternMatchingExpressions} defines pattern matching expressions; - \item \secref{ArbitraryValueExpressions} defines arbitrary value expressions; - \item \secref{StructuredTypeConstructionExpressions} defines structured type construction expressions; - \item \secref{TupleExpressions} defines tuple expressions; - \item \secref{ParenthesisedExpressions} defines parenthesised expressions; - \item \secref{ArrayConstructionExpressions} defines array construction expressions; - \item \secref{SideEffectFreeExpressions} defines \sideeffectfreeexpressionsterm{}; - \item \secref{ExprList} defines the dynamic semantics of a list of expressions. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Expressions} +\FormalRelationsDef[defines the formal relations for expressions;]{Expressions} \paragraph{Syntax:} Expressions are grammatically derived from $\Nexpr$. \paragraph{Abstract Syntax:} Expressions are derived in the abstract syntax from $\expr$, @@ -67,7 +45,8 @@ \chapter{Expressions\label{chap:Expressions}} \paragraph{Semantics:} \RenderRelation{eval_expr} \hypertarget{def-literalexpressionterm}{} -\section{Literal Expressions\label{sec:LiteralExpressions}} +\SectionDef[defines \literalexpressionsterm;] + {LiteralExpressions}{Literal Expressions} A literal expression represents a literal as an expression. \ASLListing{Literal Expressions}{literalssemantics}{\semanticstests/SemanticsRule.Lit.asl} @@ -107,7 +86,8 @@ \subsection{Semantics} \CodeSubsection{\EvalELitBegin}{\EvalELitEnd}{../Interpreter.ml} \hypertarget{def-variableexpressionterm}{} -\section{Variable Expressions\label{sec:VariableExpressions}} +\SectionDef[defines \variableexpressionsterm;] + {VariableExpressions}{Variable Expressions} A variable expression consists of an identifier for a storage element. \subsection{Syntax} @@ -162,7 +142,8 @@ \subsubsection{Comments} \TypingRuleRef{DeclareGlobalStorage}, and \TypingRuleRef{DeclareOneFunc}. \hypertarget{def-binopexpressionterm}{} -\section{Binary Expressions\label{sec:BinaryExpressions}} +\SectionDef[defines \binopexpressionsterm;] + {BinaryExpressions}{Binary Expressions} Binary expressions apply a binary operator to two sub-expressions. \RequirementDef{BinaryOperatorPriorities} @@ -540,7 +521,8 @@ \subsubsection{Comments} as well as \texttt{==}). \hypertarget{def-unopexpressionterm}{} -\section{Unary Expressions\label{sec:UnaryExpressions}} +\SectionDef[defines \unopexpressionsterm;] + {UnaryExpressions}{Unary Expressions} \subsection{Syntax} \begin{flalign*} \Nexpr \derives\ & \Nunop \parsesep \Nexpr & @@ -579,7 +561,8 @@ \subsection{Semantics} \CodeSubsection{\EvalUnopBegin}{\EvalUnopEnd}{../Interpreter.ml} \hypertarget{def-conditionexpressionterm}{} -\section{Conditional Expressions\label{sec:ConditionalExpressions}} +\SectionDef[defines \condexpressionsterm;] + {ConditionalExpressions}{Conditional Expressions} \subsection{Syntax} \begin{flalign*} \Nexpr \derives\ & \Tif \parsesep \Nexpr \parsesep \Tthen \parsesep \Nexpr \parsesep \Telse \parsesep \Nexpr &\\ @@ -645,7 +628,8 @@ \subsection{Semantics} \CodeSubsection{\EvalECondBegin}{\EvalECondEnd}{../Interpreter.ml} \hypertarget{def-callexpressionterm}{} -\section{Call Expressions\label{sec:CallExpressions}} +\SectionDef[defines \callexpressionsterm;] + {CallExpressions}{Call Expressions} \ASLListing{Call expressions}{semantics-ecall}{\semanticstests/SemanticsRule.ECall.asl} \subsection{Syntax} @@ -752,7 +736,8 @@ \subsection{Semantics} \CodeSubsection{\EvalECallBegin}{\EvalECallEnd}{../Interpreter.ml} \hypertarget{def-slicingexpressionsterm}{} -\section{Slicing Expressions\label{sec:SlicingExpressions}} +\SectionDef[defines \slicingexpressionsterm;] + {SlicingExpressions}{Slicing Expressions} This section details the high-level form of the syntax and abstract syntax of slicing expressions, and defines the semantics of bitvector slices. The details of the various types of bitvector slices are deferred to \chapref{BitvectorSlicing}. @@ -825,7 +810,8 @@ \subsection{Semantics} \hypertarget{def-arrayaccessexpressionsterm}{} \hypertarget{def-getarrayexpressionterm}{} -\section{Array Access Expressions\label{sec:ArrayAccessExpressions}} +\SectionDef[defines \arrayaccessexpressionsterm;] + {ArrayAccessExpressions}{Array Access Expressions} This section details the syntax, abstract syntax, semantics, and typing of array read expressions. \subsection{Syntax} @@ -890,7 +876,8 @@ \subsection{Abstract Syntax} \CodeSubsection{\EvalEGetArrayBegin}{\EvalEGetArrayEnd}{../Interpreter.ml} \hypertarget{def-getfieldexpressionterm}{} -\section{Field Reading Expressions\label{sec:FieldReadingExpressions}} +\SectionDef[defines field reading expressions;] + {FieldReadingExpressions}{Field Reading Expressions} \subsection{Syntax} \begin{flalign*} \Nexpr \derives\ & \Nexpr \parsesep \Tdot \parsesep \Tidentifier& @@ -1000,7 +987,8 @@ \subsection{Semantics} \CodeSubsection{\EvalEGetTupleItemBegin}{\EvalEGetTupleItemEnd}{../Interpreter.ml} \hypertarget{def-getfieldsexpressionterm}{} -\section{Multi-field Reading Expressions\label{sec:MultiFieldReadingExpressions}} +\SectionDef[defines multi-field reading expressions;] + {MultiFieldReadingExpressions}{Multi-field Reading Expressions} \subsection{Syntax} \begin{flalign*} \Nexpr \derives\ & \Nexpr \parsesep \Tdot \parsesep \Tlbracket \parsesep \ClistOne{\Tidentifier} \parsesep \Trbracket & @@ -1100,8 +1088,8 @@ \subsection{Semantics} \CodeSubsection{\EvalEGetCollectionFieldsBegin}{\EvalEGetCollectionFieldsEnd}{../Interpreter.ml} \hypertarget{def-atceexpressionterm}{} -\section{Asserting Type Conversion Expressions\label{sec:AssertingTypeConversionExpressions}} - +\SectionDef[defines asserting type conversion expressions;] + {AssertingTypeConversionExpressions}{Asserting Type Conversion Expressions} The rule about domains in the definitions of subtype-satisfaction and type-satisfaction means that it is illegal to use the unconstrained integer where a constrained integer is expected. @@ -1273,7 +1261,8 @@ \subsubsection{Comments} \RenderProseAndFormally{is_constraint_sat} \hypertarget{def-patternexpressionterm}{} -\section{Pattern Matching Expressions\label{sec:PatternMatchingExpressions}} +\SectionDef[defines pattern matching expressions;] + {PatternMatchingExpressions}{Pattern Matching Expressions} The binary operator $\Tin$ tests whether a value (referred to as the discriminant) matches any item from a $\Npatternset$. Patterns can also be used to test whether an expression matches a bitmask. Lists of patterns are also used in case statements. @@ -1357,7 +1346,8 @@ \subsection{Semantics} \CodeSubsection{\EvalEPatternBegin}{\EvalEPatternEnd}{../Interpreter.ml} \hypertarget{def-arbitraryexpressionterm}{} -\section{Arbitrary Value Expressions\label{sec:ArbitraryValueExpressions}} +\SectionDef[defines arbitrary value expressions;] + {ArbitraryValueExpressions}{Arbitrary Value Expressions} An expression of the form \texttt{ARBITRARY: ty} evaluates to an arbitrary value in the domain of \texttt{ty}. Each evaluation can produce a different arbitrary value, but (as always) once a particular expression is evaluated, its arbitrary value cannot change. @@ -1426,7 +1416,8 @@ \subsubsection{Comments} Notice that this rule introduces non-determinism. -\section{Structured Type Construction Expressions\label{sec:StructuredTypeConstructionExpressions}} +\SectionDef[defines structured type construction expressions;] + {StructuredTypeConstructionExpressions}{Structured Type Construction Expressions} \hypertarget{def-recordexpressionterm}{} \listingref{semantics-egetfield} shows an example of a well-typed record construction expression. @@ -1520,7 +1511,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_expr_ERecord} \CodeSubsection{\EvalERecordBegin}{\EvalERecordEnd}{../Interpreter.ml} -\section{Tuple Expressions\label{sec:TupleExpressions}} +\SectionDef[defines tuple expressions;] + {TupleExpressions}{Tuple Expressions} \hypertarget{def-tupleexpressionterm}{} \ASLListing{Tuple expressions}{TupleExpressions}{\definitiontests/TupleExpressions.asl} @@ -1562,7 +1554,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_expr_ETuple} \CodeSubsection{\EvalETupleBegin}{\EvalETupleEnd}{../Interpreter.ml} -\section{Parenthesised Expressions\label{sec:ParenthesisedExpressions}} +\SectionDef[defines parenthesised expressions;] + {ParenthesisedExpressions}{Parenthesised Expressions} A single expression inside parentheses is not considered to be a tuple, but rather the element inside the parenthesis. Parenthesising an expression can be used to improve readability, enforce a bracketing @@ -1594,7 +1587,8 @@ \subsection{Abstract Syntax} } \end{mathpar} -\section{Array Construction Expressions\label{sec:ArrayConstructionExpressions}} +\SectionDef[defines array construction expressions;] + {ArrayConstructionExpressions}{Array Construction Expressions} Array construction expression are used by the type system to express the initialisation of array-typed variables. Since there is no syntax to initialise arrays, there are also no rules for building the AST for such expressions nor rules for typechecking them. @@ -1620,7 +1614,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_expr_EArray} \CodeSubsection{\EvalEArrayBegin}{\EvalEArrayEnd}{../Interpreter.ml} -\section{Side-effect-free Expressions\label{sec:SideEffectFreeExpressions}} +\SectionDef[defines \sideeffectfreeexpressionsterm{};] + {SideEffectFreeExpressions}{Side-effect-free Expressions} \subsection{Typing} \texthypertarget{def-sideeffectfreeexpressionterm} An expression $\ve$ is considered to be \sideeffectfreeterm{} in the \staticenvironmentterm{} $\tenv$ @@ -1640,7 +1635,8 @@ \subsection{Semantics} Notice that the output configuration does not contain an environment, since \sideeffectfreeexpressionsterm{} do not modify the environment. -\section{Evaluating a List of Expressions\label{sec:ExprList}} +\SectionDef[defines the dynamic semantics of a list of expressions.] + {ExprList}{Evaluating a List of Expressions} \SemanticsRuleDef{EExprList} \RenderRelation{eval_expr_list} diff --git a/asllib/doc/GlobalPragmas.tex b/asllib/doc/GlobalPragmas.tex index 1dcd5e6ba5..68242d11f1 100644 --- a/asllib/doc/GlobalPragmas.tex +++ b/asllib/doc/GlobalPragmas.tex @@ -16,16 +16,9 @@ \chapter{Global Pragma Declarations\label{chap:Global Pragma Declarations}} \ASLListing{Warning of pragmas not recognised by tools}{GlobalPragma2}{\definitiontests/GlobalPragma2.asl} \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Global Pragma Declarations} defines the formal relations for global pragma declarations; - \item \SyntaxRef{Global Pragma Declarations} defines the syntax of global pragma declarations; - \item \AbstractSyntaxRef{Global Pragma Declarations} defines the abstract syntax of global pragma declarations; and - \item \TypeRulesRef{Global Pragma Declarations} defines the type rules for global pragma declarations. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Global Pragma Declarations} - +\FormalRelationsDef[defines the formal relations for global pragma declarations;]{Global Pragma Declarations} \paragraph{Syntax:} Global pragma declarations are grammatically derived from $\Ndecl$. \paragraph{Abstract Syntax:} Global pragma declarations are derived in the abstract syntax from $\decl$, @@ -37,7 +30,7 @@ \chapter{Global Pragma Declarations\label{chap:Global Pragma Declarations}} they have no associated dynamic semantics. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef{Global Pragma Declarations} +\SyntaxDef[defines the syntax of global pragma declarations;]{Global Pragma Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{flalign*} @@ -45,7 +38,7 @@ \chapter{Global Pragma Declarations\label{chap:Global Pragma Declarations}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Global Pragma Declarations} +\AbstractSyntaxDef[defines the abstract syntax of global pragma declarations; and]{Global Pragma Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RenderTypes[remove_hypertargets]{decl_global_pragma} @@ -66,7 +59,7 @@ \chapter{Global Pragma Declarations\label{chap:Global Pragma Declarations}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef{Global Pragma Declarations} +\TypeRulesDef[defines the type rules for global pragma declarations.]{Global Pragma Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \TypingRuleDef{CheckGlobalPragma} diff --git a/asllib/doc/GlobalStorageDeclarations.tex b/asllib/doc/GlobalStorageDeclarations.tex index 92e3663816..4f941107d7 100644 --- a/asllib/doc/GlobalStorageDeclarations.tex +++ b/asllib/doc/GlobalStorageDeclarations.tex @@ -7,19 +7,11 @@ \chapter{Global Storage Declarations\label{chap:GlobalStorageDeclarations}} \ASLListing{Examples of global storage declarations}{GlobalStorageDeclarations}{\definitiontests/GlobalStorageDeclarations.asl} \ChapterOutline -\begin{itemize} - \item \secref{ConfigurableGlobalStorageDeclarations} describes configurable global storage elements --- - elements declared with the \Tconfig{} keyword; - \item \FormalRelationsRef{Global Storage Declarations} defines the formal relations - for global storage declarations; - \item \SyntaxRef{Global Storage Declarations} defines the syntax of global storage declarations; - \item \AbstractSyntaxRef{Global Storage Declarations} defines the abstract syntax of global storage declarations; - \item \TypeRulesRef{Global Storage Declarations} defines the type rules of global storage declarations; - \item \SemanticsRulesRef{Global Storage Declarations} defines the dynamic semantics of global storage declarations. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Configurable Global Storage Declarations\label{sec:ConfigurableGlobalStorageDeclarations}} +\SectionDef[describes configurable global storage elements --- + elements declared with the \Tconfig{} keyword;] + {ConfigurableGlobalStorageDeclarations}{Configurable Global Storage Declarations} Global storage declarations with the keyword \texttt{config} aim to assist implementation-specific support for ``configuration'' of an ASL specification. In particular, implementations may provide mechanisms to override \texttt{config} values, such as: \begin{itemize} @@ -39,7 +31,8 @@ \section{Configurable Global Storage Declarations\label{sec:ConfigurableGlobalSt \end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Global Storage Declarations} +\FormalRelationsDef[defines the formal relations + for global storage declarations;]{Global Storage Declarations} \paragraph{Syntax:} Global storage declarations are grammatically derived from $\Ndecl$ via the subset of productions shown in \SyntaxRef{Global Storage Declarations}. @@ -54,8 +47,7 @@ \section{Configurable Global Storage Declarations\label{sec:ConfigurableGlobalSt The semantics of a single global storage declaration is defined in \SemanticsRuleRef{DeclareGlobal}. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef{Global Storage Declarations} - +\SyntaxDef[defines the syntax of global storage declarations;]{Global Storage Declarations} \RequirementDef{DiscardingGlobalStorageDeclarations} Global storage declarations must\\ bind a name. This is ensured by the ASL grammar. @@ -78,7 +70,7 @@ \section{Configurable Global Storage Declarations\label{sec:ConfigurableGlobalSt \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Global Storage Declarations} +\AbstractSyntaxDef[defines the abstract syntax of global storage declarations;]{Global Storage Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RenderTypes[remove_hypertargets]{decl_global_storage} @@ -250,7 +242,7 @@ \section{Configurable Global Storage Declarations\label{sec:ConfigurableGlobalSt \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef{Global Storage Declarations} +\TypeRulesDef[defines the type rules of global storage declarations;]{Global Storage Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RequirementDef{GlobalStorageCycles} @@ -369,7 +361,7 @@ \section{Configurable Global Storage Declarations\label{sec:ConfigurableGlobalSt \end{TypingRuleList} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SemanticsRulesDef{Global Storage Declarations} +\SemanticsRulesDef[defines the dynamic semantics of global storage declarations.]{Global Storage Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% This section defines the following relations: diff --git a/asllib/doc/LexicalStructure.tex b/asllib/doc/LexicalStructure.tex index 6be5c8fe9e..e7d04bee47 100644 --- a/asllib/doc/LexicalStructure.tex +++ b/asllib/doc/LexicalStructure.tex @@ -6,22 +6,9 @@ \chapter{Lexical Structure\label{chap:LexicalStructure}} either a list of \emph{tokens} or a lexical error. \ChapterOutline -\begin{itemize} - \item \secref{ASL Specification Text} defines what constitutes the text of an ASL specification, - \item \secref{Lexical Regular Expressions} defines the regular expressions used to define the lexical structure, - \item \secref{Whitespace} defines whitespace, - \item \secref{Comments} defines comments, - \item \secref{Integer Literals} defines integer literals, - \item \secref{Rational Number Literals} defines rational number literals, - \item \secref{Boolean Literals} defines Boolean literals, - \item \secref{Bitvector Literals} defines bitvector literals, - \item \secref{Bitmasks} defines bitmasks, - \item \secref{String Literals} defines string literals, - \item \secref{LexicalIdentifiers} defines identifiers, and - \item \secref{LexicalAnalysis} defines the analysis used to transform text into tokens. -\end{itemize} -\section{ASL Specification Text\label{sec:ASL Specification Text}} +\SectionDef[defines what constitutes the text of an ASL specification,] + {ASL Specification Text}{ASL Specification Text} An ASL specification is a string, that is a list of ASCII characters, consisting of a \emph{content text} followed by an \emph{end-of-file}. The content text is a list of @@ -37,8 +24,8 @@ \section{ASL Specification Text\label{sec:ASL Specification Text}} % NO_EXAMPLE In particular, it is an error to use a tab character in ASL specification text (decimal encoding 9). -\section{Lexical Regular Expressions\label{sec:Lexical Regular Expressions}} - +\SectionDef[defines the regular expressions used to define the lexical structure,] + {Lexical Regular Expressions}{Lexical Regular Expressions} \hypertarget{def-regex}{} \taref{LexicalRegularExpressions} defines the regular expressions $\RegExp$ used to define \emph{lexemes} --- substrings of the ASL specification text that are used to form \emph{tokens}. @@ -86,7 +73,8 @@ \section{Lexical Regular Expressions\label{sec:Lexical Regular Expressions}} The notation $\Lang{e}$ stands for the \emph{formal language} of a regular expression $e$. That is, the set of strings that match that regular expression. -\section{Whitespace\label{sec:Whitespace}} +\SectionDef[defines whitespace,] + {Whitespace}{Whitespace} \RequirementDef{Whitespace} Comments and whitespace characters are collectively referred to as whitespace lexemes and are discarded. Technically, line comments and multi-line comments are treated @@ -108,7 +96,8 @@ \section{Whitespace\label{sec:Whitespace}} \end{tabular} \end{center} -\section{Comments\label{sec:Comments}} +\SectionDef[defines comments,] + {Comments}{Comments} ASL supports comments in the style of C++: \begin{itemize} \item Single-line comments: the text from \text{//} until the end of the line @@ -130,7 +119,8 @@ \section{Comments\label{sec:Comments}} Multi-line comments are defined by \hyperlink{start-multiline-comment}{intercepting \texttt{"/*"}} (see \secref{scanningmultilinecomments}). -\section{Integer Literals\label{sec:Integer Literals}} +\SectionDef[defines integer literals,] + {Integer Literals}{Integer Literals} Integers are written either in decimal using one or more of the characters \texttt{0-9} and underscore, or in hexadecimal using \texttt{0x} at the start followed by the characters \texttt{0-9, a-f, A-F} and underscore. An integer literal cannot start with an underscore. @@ -154,7 +144,8 @@ \section{Integer Literals\label{sec:Integer Literals}} \end{tabular} \end{center} -\section{Rational Number Literals\label{sec:Rational Number Literals}} +\SectionDef[defines rational number literals,] + {Rational Number Literals}{Rational Number Literals} Rational numbers are written in decimal form and consist of one or more decimal digits, a decimal point, and one or more decimal digits. Underscores can be added between digits to aid readability. @@ -176,10 +167,12 @@ \section{Rational Number Literals\label{sec:Rational Number Literals}} \end{tabular} \end{center} -\section{Boolean Literals\label{sec:Boolean Literals}} +\SectionDef[defines Boolean literals,] + {Boolean Literals}{Boolean Literals} Boolean literals are written using \texttt{TRUE} or \texttt{FALSE}. -\section{Bitvector Literals\label{sec:Bitvector Literals}} +\SectionDef[defines bitvector literals,] + {Bitvector Literals}{Bitvector Literals} Constant bitvectors are written using 1, 0 and spaces surrounded by single-quotes. We first define a regular expression for a bit character: @@ -210,7 +203,8 @@ \section{Bitvector Literals\label{sec:Bitvector Literals}} For example, in \verb|'10100'| the \ProseMSB{} is \verb|1| at index $4$, and the \ProseLSB{} is \verb|0| at index $0$. -\section{Bitmasks\label{sec:Bitmasks}} +\SectionDef[defines bitmasks,] + {Bitmasks}{Bitmasks} Constant bitmasks are written using \texttt{1}, \texttt{0}, \texttt{x}, and \texttt{0}s/\texttt{1}s enclosed in parentheses. Any \texttt{x}s or characters enclosed in parentheses represent don't care characters. @@ -232,7 +226,8 @@ \section{Bitmasks\label{sec:Bitmasks}} Bitmasks follow \RequirementRef{BitvectorOrdering}. -\section{String Literals\label{sec:String Literals}} +\SectionDef[defines string literals,] + {String Literals}{String Literals} String literals consist of printable characters surrounded by double quotes. They are used to create string values, which are strings of zero or more characters, where a character is a printable ASCII character, @@ -269,7 +264,8 @@ \section{String Literals\label{sec:String Literals}} \end{tabular} \end{center} -\section{Identifiers\label{sec:LexicalIdentifiers}} +\SectionDef[defines identifiers, and] + {LexicalIdentifiers}{Identifiers} Identifiers start with a letter or underscore and continue with zero or more letters, underscores or digits. Identifiers are case sensitive. \hypertarget{def-reletter}{} @@ -327,7 +323,8 @@ \section{Identifiers\label{sec:LexicalIdentifiers}} can be useful for declaring a constant specific to the platform \verb|my_platform|. \ASLListing{An identifier starting with a single underscore}{IdentifierSingleUnderscore}{\syntaxtests/ConventionRule.IdentifierSingleUnderscore.asl} -\section{Lexical Analysis\label{sec:LexicalAnalysis}} +\SectionDef[defines the analysis used to transform text into tokens.] + {LexicalAnalysis}{Lexical Analysis} Lexical analysis, which is also referred to as \emph{scanning}, is defined via the function \hypertarget{def-aslscan}{} \[ diff --git a/asllib/doc/Literals.tex b/asllib/doc/Literals.tex index bf11b6fb44..929f6dfe18 100644 --- a/asllib/doc/Literals.tex +++ b/asllib/doc/Literals.tex @@ -16,16 +16,9 @@ \chapter{Literals\label{chap:Literals}} \ASLListing{Examples of literals and their corresponding types}{literals1}{\typingtests/TypingRule.Lit.asl} \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Literals} defines the formal relations for literals; - \item \SyntaxRef{Literals} defines the syntax for literals; - \item \AbstractSyntaxRef{Literals} defines the abstract syntax and the abstract syntax builders for literals; - \item \TypeRulesRef{Literals} defines the typing of literals; and - \item \SemanticsRulesRef{Literals} defines the semantics of literals. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Literals} +\FormalRelationsDef[defines the formal relations for literals;]{Literals} \paragraph{Syntax:} Literals are grammatically derived from $\Nvalue$. \paragraph{Abstract Syntax:} Literals are derived in abstract syntax from $\literal$. The function $\buildvalue$ transforms a parse node for $\Nvalue$, except for enumeration labels, @@ -35,7 +28,7 @@ \chapter{Literals\label{chap:Literals}} (see \SemanticsRulesRef{Literals}). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef{Literals} +\SyntaxDef[defines the syntax for literals;]{Literals} \begin{flalign*} \Nvalue \derives \ & \Tintlit &\\ |\ & \Tboollit &\\ @@ -45,7 +38,7 @@ \chapter{Literals\label{chap:Literals}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Literals} +\AbstractSyntaxDef[defines the abstract syntax and the abstract syntax builders for literals;]{Literals} \RenderType[remove_hypertargets]{literal} \subsection{ASTRule.Value \label{sec:ASTRule.Value}} @@ -95,7 +88,7 @@ \subsection{ASTRule.Value \label{sec:ASTRule.Value}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef{Literals} +\TypeRulesDef[defines the typing of literals; and]{Literals} See \ExampleRef{Literals}. \TypingRuleDef{Lit} @@ -106,7 +99,7 @@ \subsection{ASTRule.Value \label{sec:ASTRule.Value}} \CodeSubsection{\LitBegin}{\LitEnd}{../Typing.ml} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SemanticsRulesDef{Literals} +\SemanticsRulesDef[defines the semantics of literals.]{Literals} A literal $\vl$ is represented in the dynamic semantics by the \nativevalueterm{} $\NVLiteral(\vl)$. \ExampleDef{Converting a Literal to a Value} diff --git a/asllib/doc/LocalStorageDeclarations.tex b/asllib/doc/LocalStorageDeclarations.tex index b473126922..6982cac466 100644 --- a/asllib/doc/LocalStorageDeclarations.tex +++ b/asllib/doc/LocalStorageDeclarations.tex @@ -9,18 +9,9 @@ \chapter{Local Storage Declarations\label{chap:LocalStorageDeclarations}} \ASLListing{Local storage declarations}{LocalStorageDeclarations}{\definitiontests/LocalStorageDeclarations.asl} \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Local Storage Declarations} defines the formal relations for local storage declarations; - \item \SyntaxRef{Local Storage Declarations} defines the syntax of local storage declarations; - \item \AbstractSyntaxRef{Local Storage Declarations} defines the abstract syntax of local storage declarations; - \item \secref{Typing of Local Variable Declarations} defines the type rules of local variable declarations; - \item \secref{Semantics of Local Variable Declarations} defines the dynamic semantics of local variable declarations; - \item \secref{Typing of Tuple Declarations} defines the type rules of tuples of local storage declarations; - \item \secref{Semantics of Tuple Declarations} defines the dynamic semantics of tuples of local storage declarations. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Local Storage Declarations} +\FormalRelationsDef[defines the formal relations for local storage declarations;]{Local Storage Declarations} \paragraph{Syntax:} Local storage declarations are grammatically derived from statements ($\Nstmt$) via dedicated rules (see \SyntaxRef{Local Storage Declarations}). @@ -40,7 +31,7 @@ \chapter{Local Storage Declarations\label{chap:LocalStorageDeclarations}} This is used to evaluate both single local storage declarations and tuples of local storage declarations. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef{Local Storage Declarations} +\SyntaxDef[defines the syntax of local storage declarations;]{Local Storage Declarations} \hypertarget{def-localdeclarationkeyword}{} \hypertarget{def-localdeclarationitem}{} A \localdeclarationkeyword\ is either \texttt{var} or \texttt{let}. @@ -64,7 +55,7 @@ \chapter{Local Storage Declarations\label{chap:LocalStorageDeclarations}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Local Storage Declarations} +\AbstractSyntaxDef[defines the abstract syntax of local storage declarations;]{Local Storage Declarations} \RenderTypes[remove_hypertargets]{local_decl_keyword_and_item} @@ -160,7 +151,8 @@ \chapter{Local Storage Declarations\label{chap:LocalStorageDeclarations}} } \end{mathpar} -\section{Typing of Local Variable Declarations\label{sec:Typing of Local Variable Declarations}} +\SectionDef[defines the type rules of local variable declarations;] + {Typing of Local Variable Declarations}{Typing of Local Variable Declarations} \TypingRuleDef{LDVar} \ExampleDef{Well-typed Local Variable Declarations} In \listingref{ldvar}, the statement \texttt{let x = 3;} is legal, since @@ -208,7 +200,8 @@ \section{Typing of Local Variable Declarations\label{sec:Typing of Local Variabl \CodeSubsection{\CheckIsNotCollectionBegin}{\CheckIsNotCollectionEnd}{../Typing.ml} -\section{Semantics of Local Variable Declarations\label{sec:Semantics of Local Variable Declarations}} +\SectionDef[defines the dynamic semantics of local variable declarations;] + {Semantics of Local Variable Declarations}{Semantics of Local Variable Declarations} \SemanticsRuleDef{LDVar} \ExampleDef{Evaluation of a Local Variable Declaration} The statement \texttt{var x = 3;} in \listingref{ldvar} binds \texttt{x} @@ -218,7 +211,8 @@ \section{Semantics of Local Variable Declarations\label{sec:Semantics of Local V \RenderProseAndFormally{eval_local_decl_LDI_Var} \CodeSubsection{\EvalLDVarBegin}{\EvalLDVarEnd}{../Interpreter.ml} -\section{Typing of Tuple Declarations\label{sec:Typing of Tuple Declarations}} +\SectionDef[defines the type rules of tuples of local storage declarations;] + {Typing of Tuple Declarations}{Typing of Tuple Declarations} \TypingRuleDef{LDTuple} \ExampleDef{Well-typed Tuple Declarations} \ASLListing{Declaring a tuple in the local storage}{typing-ldtuple}{\typingtests/TypingRule.LDTuple.asl} @@ -234,7 +228,8 @@ \section{Typing of Tuple Declarations\label{sec:Typing of Tuple Declarations}} \RenderProseAndFormally{add_local_vars} -\section{Semantics of Tuple Declarations\label{sec:Semantics of Tuple Declarations}} +\SectionDef[defines the dynamic semantics of tuples of local storage declarations.] + {Semantics of Tuple Declarations}{Semantics of Tuple Declarations} \SemanticsRuleDef{LDTuple} \ExampleDef{Evaluation of Tuple Declarations} In \listingref{semantics-ldtuple}, diff --git a/asllib/doc/PatternMatching.tex b/asllib/doc/PatternMatching.tex index d013a02a7e..0b4441b9cb 100644 --- a/asllib/doc/PatternMatching.tex +++ b/asllib/doc/PatternMatching.tex @@ -9,19 +9,9 @@ \chapter{Pattern Matching\label{chap:PatternMatching}} \ASLListing{Examples of patterns}{Patterns}{\definitiontests/Patterns.asl} \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Patterns} defines the formal relations for patterns; - \item \secref{MatchingAllValues} defines the match-all-values pattern; - \item \secref{MatchingASingleValue} defines the match-a-single-value pattern; - \item \secref{MatchingARangeOfIntegers} defines the match-a-range-of-integers pattern; - \item \secref{MatchingAnUpperBoundedRangeOfIntegers} defines the match-integers-less-than pattern; - \item \secref{MatchingALowerBoundedRangeOfIntegers} defines the match-integers-greater-than pattern; - \item \secref{MatchingABitmask} defines the bitmask pattern; - \item \secref{MatchingPatternLists} defines positive and negative matching against pattern lists. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Patterns} +\FormalRelationsDef[defines the formal relations for patterns;]{Patterns} \paragraph{Syntax:} Patterns are grammatically derived from $\Npattern$. \paragraph{Abstract Syntax:} Patterns are derived in the abstract grammar from $\pattern$ @@ -39,7 +29,8 @@ \chapter{Pattern Matching\label{chap:PatternMatching}} \paragraph{Semantics:} Patterns are evaluated by $\evalpattern$. \RenderRelation{eval_pattern} -\section{Matching All Values\label{sec:MatchingAllValues}} +\SectionDef[defines the match-all-values pattern;] + {MatchingAllValues}{Matching All Values} \hypertarget{any-pattern}{} \ASLListing{Matching any value}{semantics-pall}{\semanticstests/SemanticsRule.PAll.asl} @@ -76,7 +67,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_pattern_PAll} \CodeSubsection{\EvalPAllBegin}{\EvalPAllEnd}{../Interpreter.ml} -\section{Matching a Single Value\label{sec:MatchingASingleValue}} +\SectionDef[defines the match-a-single-value pattern;] + {MatchingASingleValue}{Matching a Single Value} \subsection{Syntax} \begin{flalign*} \Npattern \derives\ & \Nexpr & @@ -117,7 +109,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_pattern_PSingle} \CodeSubsection{\EvalPSingleBegin}{\EvalPSingleEnd}{../Interpreter.ml} -\section{Matching a Range of Integers\label{sec:MatchingARangeOfIntegers}} +\SectionDef[defines the match-a-range-of-integers pattern;] + {MatchingARangeOfIntegers}{Matching a Range of Integers} \subsection{Syntax} \begin{flalign*} \Npattern \derives\ & \Nexpr \parsesep \Tslicing \parsesep \Nexpr & @@ -165,7 +158,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_pattern_PRange} \CodeSubsection{\EvalPRangeBegin}{\EvalPRangeEnd}{../Interpreter.ml} -\section{Matching an Upper Bounded Range of Integers\label{sec:MatchingAnUpperBoundedRangeOfIntegers}} +\SectionDef[defines the less-than-or-equal pattern;] + {MatchingAnUpperBoundedRangeOfIntegers}{Matching an Upper Bounded Range of Integers} \subsection{Syntax} \begin{flalign*} \Npattern \derives\ & \Tleq \parsesep \Nexpr & @@ -207,7 +201,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_pattern_PLeq} \CodeSubsection{\EvalPLeqBegin}{\EvalPLeqEnd}{../Interpreter.ml} -\section{Matching a Lower Bounded Range of Integers\label{sec:MatchingALowerBoundedRangeOfIntegers}} +\SectionDef[defines the greater-than-or-equal pattern;] + {MatchingALowerBoundedRangeOfIntegers}{Matching a Lower Bounded Range of Integers} \subsection{Syntax} \begin{flalign*} \Npattern \derives\ & \Tgeq \parsesep \Nexpr & @@ -249,7 +244,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_pattern_PGeq} \CodeSubsection{\EvalPGeqBegin}{\EvalPGeqEnd}{../Interpreter.ml} -\section{Matching a Bitmask\label{sec:MatchingABitmask}} +\SectionDef[defines the bitmask pattern;] + {MatchingABitmask}{Matching a Bitmask} Bitmasks are used to match sets of bitvectors where occurrences of $\xbit$, and bit sequences in parentheses represent, don't-care values. @@ -310,7 +306,8 @@ \subsection{Semantics} \CodeSubsection{\EvalPMaskBegin}{\EvalPMaskEnd}{../Interpreter.ml} -\section{Matching Pattern Lists\label{sec:MatchingPatternLists}} +\SectionDef[defines positive and negative matching against pattern lists.] + {MatchingPatternLists}{Matching Pattern Lists} Pattern-list forms are the only set-like pattern syntax. They appear at the top level of an \texttt{IN} expression or a case alternative, and their elements are simple patterns, that is, patterns derived from \Npattern. The forms \verb|{...}| and diff --git a/asllib/doc/PrimitiveOperations.tex b/asllib/doc/PrimitiveOperations.tex index d390f9b355..9d2ae8066c 100644 --- a/asllib/doc/PrimitiveOperations.tex +++ b/asllib/doc/PrimitiveOperations.tex @@ -20,20 +20,8 @@ \chapter{Primitive Operations\label{chap:PrimitiveOperations}} \ASLListing{Examples of primitive operations}{PrimitiveOperations}{\definitiontests/PrimitiveOperations.asl} \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Primitive Operations} defines the formal relations for primitive operations; - \item \SyntaxRef{Primitive Operations} defines the syntax for unary operations and binary operations; - \item \AbstractSyntaxRef{Primitive Operations} defines the AST for unary operations and binary operations; - \item \secref{PrimitiveOperationSignatures} defines the signatures for all primitive operations; - \item \secref{PrimitiveOperationDomains} defines the valid sets of operand values for primitive operations; - \item \TypeRulesRef{Primitive Operations} defines the static evaluation of primitive operations for literal values; - \item \SemanticsRulesRef{Primitive Operations} defines how to adapt the static evaluation of the primitive operations - (given by $\unopliterals$ and $\binopliterals$) for the dynamic semantics. Essentially this is done by unwrapping - \nativevaluesterm{} into literal values, applying either $\unopliterals$ or $\binopliterals$, - and finally wrapping the results by \nativevaluesterm{}. -\end{itemize} -\FormalRelationsDef{Primitive Operations} +\FormalRelationsDef[defines the formal relations for primitive operations;]{Primitive Operations} \paragraph{Syntax:} primitive operations are grammatically derived from $\Nunop$ and $\Nbinop$. \paragraph{Abstract Syntax:} primitive operations are derived in the abstract syntax from $\unop$ @@ -53,7 +41,7 @@ \chapter{Primitive Operations\label{chap:PrimitiveOperations}} and binary operations are dynamically evaluated via $\evalbinop$ (see \SemanticsRuleRef{BinopValues}). -\SyntaxDef{Primitive Operations} +\SyntaxDef[defines the syntax for unary operations and binary operations;]{Primitive Operations} \begin{flalign*} \Nunop \derivesinline\ & \Tbnot \;|\; \Tminus \;|\; \Tnot &\\ \Nbinop \derivesinline\ & \Tand \;|\; \Tband \;|\; \Tbor \;|\; \Tbeq \;|\; \Tdiv \;|\; \Tdivrm \;|\; \Txor \;|\; \Teqop \;|\; \Tneq &\\ @@ -61,7 +49,7 @@ \chapter{Primitive Operations\label{chap:PrimitiveOperations}} |\ & \Tor \;|\; \Trdiv \;|\; \Tshl \;|\; \Tshr \;|\; \Tpow \;|\; \Tcoloncolon \;|\; \Tplusplus \end{flalign*} -\AbstractSyntaxDef{Primitive Operations} +\AbstractSyntaxDef[defines the AST for unary operations and binary operations;]{Primitive Operations} \RenderTypes[remove_hypertargets]{unop_and_binop} @@ -255,7 +243,8 @@ \chapter{Primitive Operations\label{chap:PrimitiveOperations}} } \end{mathpar} -\section{Primitive Operation Signatures\label{sec:PrimitiveOperationSignatures}} +\SectionDef[defines the signatures for all primitive operations;] + {PrimitiveOperationSignatures}{Primitive Operation Signatures} ASL follows the mathematical and programming language tradition of allowing operators such as \texttt{+} to be overloaded to refer to one of several different operations. % @@ -501,7 +490,8 @@ \section{Primitive Operation Signatures\label{sec:PrimitiveOperationSignatures}} \end{table} \clearpage -\section{Primitive Operation Domains\label{sec:PrimitiveOperationDomains}} +\SectionDef[defines the valid sets of operand values for primitive operations;] + {PrimitiveOperationDomains}{Primitive Operation Domains} The unary operations ($\aslnotbool$, $\negateint$, $\negatereal$, and $\notbits$) are valid for all possible literal values, and most binary operations are also valid for all possible combinations of literal values of their operands. However, some binary operations are only considered valid for a subset of possible operand values. @@ -539,7 +529,7 @@ \section{Primitive Operation Domains\label{sec:PrimitiveOperationDomains}} \end{tabular} \end{center} -\TypeRulesDef{Primitive Operations} +\TypeRulesDef[defines the static evaluation of primitive operations for literal values;]{Primitive Operations} \TypingRuleDef{UnopLiterals} \RenderRelation{unop_literals} @@ -795,8 +785,10 @@ \subsubsection{Operators Over String Values \label{sec:StringOperations}} \subsubsection{Operators Over Label Values \label{sec:LabelOperations}} \RenderProseAndFormally{binop_literals_label} -\SemanticsRulesDef{Primitive Operations} - +\SemanticsRulesDef[defines how to adapt the static evaluation of the primitive operations + (given by $\unopliterals$ and $\binopliterals$) for the dynamic semantics. Essentially this is done by unwrapping + \nativevaluesterm{} into literal values, applying either $\unopliterals$ or $\binopliterals$, + and finally wrapping the results by \nativevaluesterm{}.]{Primitive Operations} \SemanticsRuleDef{UnopValues} \RenderRelation{eval_unop} diff --git a/asllib/doc/RelationsOnTypes.tex b/asllib/doc/RelationsOnTypes.tex index df393feb7a..03cebdfc0c 100644 --- a/asllib/doc/RelationsOnTypes.tex +++ b/asllib/doc/RelationsOnTypes.tex @@ -1,5 +1,6 @@ -\section{Relations Over Types\label{sec:RelationsOnTypes}} - +\SectionDef[defines relations on types that are needed to typecheck + expressions and statements; and] + {RelationsOnTypes}{Relations Over Types} This section defines the following relations over types and operators: \begin{itemize} \item Subtype Satisfaction (\TypingRuleRef{SubtypeSatisfaction}) diff --git a/asllib/doc/Semantics.tex b/asllib/doc/Semantics.tex index 944eecf10e..689d8b7ca6 100644 --- a/asllib/doc/Semantics.tex +++ b/asllib/doc/Semantics.tex @@ -23,18 +23,10 @@ \chapter{Dynamic Semantics Definitions\label{chap:Semantics}} of the ASL dynamic semantics appears in \chapref{FormalSystem}. \ChapterOutline -\begin{itemize} - \item \secref{MeaningfulASLSpecifications} explains which ASL specifications have a dynamic semantics - assigned to them; - \item \secref{Sequential Semantics and Dynamic Semantics} explains how this reference defines both the - sequential semantics and concurrent semantics for ASL; - \item \secref{Dynamic Semantics Configurations} defines the configurations used by the dynamic semantics; - \item \secref{nativevalues} defines the concept of \nativevaluesterm{}; - \item \secref{Semantic Evaluation} explains how the dynamic semantics rules are used to evaluate specifications; and - \item \secref{Semantics of Diverging Specifications} defines the semantics of diverging specifications. -\end{itemize} -\section{Meaningful ASL Specifications\label{sec:MeaningfulASLSpecifications}} +\SectionDef[explains which ASL specifications have a dynamic semantics + assigned to them;] + {MeaningfulASLSpecifications}{Meaningful ASL Specifications} The ASL dynamic semantics defined here assign meaning only to \emph{well-typed specifications}. More specifically, the semantics are only defined for a \typedast{} produced by the typechecker from some \untypedast{} (rather than a \typingerrorterm{}). @@ -53,7 +45,9 @@ \section{Meaningful ASL Specifications\label{sec:MeaningfulASLSpecifications}} the ASL dynamic semantics rules to assign meaning to both terminating specifications and diverging specifications. -\section{Sequential Semantics and Dynamic Semantics\label{sec:Sequential Semantics and Dynamic Semantics}} +\SectionDef[explains how this reference defines both the + sequential semantics and concurrent semantics for ASL;] + {Sequential Semantics and Dynamic Semantics}{Sequential Semantics and Dynamic Semantics} \hypertarget{def-semanticconfiguration}{} The ASL dynamic semantics are given by relations between \emph{\semanticsconfigurationsterm}~\cite{SemanticsWithApplicationsBook} @@ -90,7 +84,8 @@ \section{Sequential Semantics and Dynamic Semantics\label{sec:Sequential Semanti Technically, the sequential semantics are defined by omitting the concurrent execution graph components from all \semanticsconfigurationsterm{}. -\section{Dynamic Semantics Configurations\label{sec:Dynamic Semantics Configurations}} +\SectionDef[defines the configurations used by the dynamic semantics;] + {Dynamic Semantics Configurations}{Dynamic Semantics Configurations} This section defines the mathematical types over which our dynamic semantics are defined. An \hyperlink{eval-example}{example} of semantic evaluation appears at the end. @@ -119,7 +114,8 @@ \section{Dynamic Semantics Configurations\label{sec:Dynamic Semantics Configurat \hypertarget{def-nativevalue}{} \hypertarget{def-nativevalues}{} -\section{Native Values\label{sec:nativevalues}} +\SectionDef[defines the concept of \nativevaluesterm{};] + {nativevalues}{Native Values} Semantic evaluation binds values to storage elements when a specification is semantically evaluated. To formalise this, we define the set of \emph{\nativevaluesterm} as follows (\texttt{NV} stands for Native Value): @@ -449,7 +445,8 @@ \subsection{Extracting and Substituting Elements of Semantics Configurations} \] \end{small} -\section{Semantic Evaluation\label{sec:Semantic Evaluation}} +\SectionDef[explains how the dynamic semantics rules define the evaluation of ASL constructs; and] + {Semantic Evaluation}{Semantic Evaluation} \hypertarget{def-evalrel}{} The semantics of ASL is given by the relation\footnote{The reason that a relation, rather than a function, is used is due to the non-determinism inherent in the \ARBITRARY{} expression.} @@ -639,7 +636,8 @@ \subsection{Evaluation Order\label{sec:EvaluationOrder}} \end{Verbatim} % CONSOLE_END -\section{Semantics of Diverging Specifications\label{sec:Semantics of Diverging Specifications}} +\SectionDef[defines the semantics of diverging specifications.] + {Semantics of Diverging Specifications}{Semantics of Diverging Specifications} While typical specifications are intended to always terminate, diverging specifications can be potentially useful. For example, simulating the fetch-decode-execute cycle of a given processor, diff --git a/asllib/doc/SideEffects.tex b/asllib/doc/SideEffects.tex index 0bf9c478ae..5fbd588d0e 100644 --- a/asllib/doc/SideEffects.tex +++ b/asllib/doc/SideEffects.tex @@ -11,18 +11,10 @@ \chapter{Side Effects\label{chap:SideEffects}} A \symbolicallyevaluableterm{} expression is compatible with symbolic reduction and equivalence testing (see \chapref{SymbolicEquivalenceTesting}). \ChapterOutline -\begin{itemize} - \item \secref{Purity} defines the concept of expression \purities{}; - \item \secref{SideEffectDescriptors} defines \sideeffectdescriptorsetsterm, which the type system infers - for each kind of ASL construct; - \item \secref{SideEffectSets} defines functions used to construct, modify, and query sets - of \sideeffectdescriptorsetsterm{}. - These are used throughout the type system to infer \sideeffectdescriptorsetsterm{} - and to ensure each construct meets its requirements in terms of side effects. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Purity\label{sec:Purity}} +\SectionDef[defines the concept of expression \purities{};] + {Purity}{Purity} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% We now define configurations used to determine whether expressions are \pureterm{} and \readonlyterm{} by the side effect analysis, as explained below. @@ -50,7 +42,9 @@ \section{Purity\label{sec:Purity}} \] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Side Effect Descriptors\label{sec:SideEffectDescriptors}} +\SectionDef[defines \sideeffectdescriptorsetsterm, which the type system infers + for each kind of ASL construct;] + {SideEffectDescriptors}{Side Effect Descriptors} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \hypertarget{def-sideeffectdescriptorterm}{} @@ -120,7 +114,11 @@ \section{Side Effect Descriptors\label{sec:SideEffectDescriptors}} \RenderProseAndFormally{side_effect_is_symbolically_evaluable} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Side Effect Sets\label{sec:SideEffectSets}} +\SectionDef[defines functions used to construct, modify, and query sets + of \sideeffectdescriptorsetsterm{}. + These are used throughout the type system to infer \sideeffectdescriptorsetsterm{} + and to ensure each construct meets its requirements in terms of side effects.] + {SideEffectSets}{Side Effect Sets} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Transliteration note: diff --git a/asllib/doc/Slicing.tex b/asllib/doc/Slicing.tex index 21aabe1185..942d4d81c9 100644 --- a/asllib/doc/Slicing.tex +++ b/asllib/doc/Slicing.tex @@ -11,21 +11,9 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \ASLListing{Examples of bitvector slices and operations on slices}{BitvectorSlices}{\definitiontests/Bitvector_slices.asl} \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Bitvector Slices} defines the formal relations for bitvector slices; - \item \SyntaxRef{Bitvector Slices} defines the syntax of bitvector slices; - \item \AbstractSyntaxRef{Bitvector Slices} defines the abstract syntax of bitvector slices; - \item \TypeRulesRef{Bitvector Slices} defines the type rules for bitvector slices; - \item \SemanticsRulesRef{Bitvector Slices} defines the dynamic semantics of bitvector slices; - \item \FormalRelationsRef{Lists of Bitvector Slices} defines the formal relations for lists of bitvector slices; - \item \SyntaxRef{Lists of Bitvector Slices} defines the syntax of lists of bitvector slices; - \item \AbstractSyntaxRef{Lists of Bitvector Slices} defines the abstract syntax of lists of bitvector slices; - \item \TypeRulesRef{Lists of Bitvector Slices} defines the type rules for lists of bitvector slices; - \item \SemanticsRulesRef{Lists of Bitvector Slices} defines the dynamic semantics rules for lists of bitvector slices; -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Bitvector Slices} +\FormalRelationsDef[defines the formal relations for bitvector slices;]{Bitvector Slices} \paragraph{Syntax:} Bitvector slices are grammatically derived from $\Nslice$. \paragraph{Abstract Syntax:} Bitvector slices are derived in the abstract syntax from $\slice$, @@ -36,7 +24,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \paragraph{Semantics:} Bitvector slices are evaluated by $\evalslice$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef{Bitvector Slices} +\SyntaxDef[defines the syntax of bitvector slices;]{Bitvector Slices} \begin{flalign*} \Nslice \derives \ & \Nexpr &\\ |\ & \Nexpr \parsesep \Tcolon \parsesep \Nexpr &\\ @@ -44,7 +32,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Bitvector Slices} +\AbstractSyntaxDef[defines the abstract syntax of bitvector slices;]{Bitvector Slices} \RenderTypes[remove_hypertargets]{untyped_slice} \ASTRuleDef{Slice} @@ -86,7 +74,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef{Bitvector Slices} +\TypeRulesDef[defines the type rules for bitvector slices;]{Bitvector Slices} \TypingRuleDef{Slice} \RenderRelation{annotate_slice} @@ -141,7 +129,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \CodeSubsection{\SymbolicConstrainedIntegerBegin}{\SymbolicConstrainedIntegerEnd}{../Typing.ml} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SemanticsRulesDef{Bitvector Slices} +\SemanticsRulesDef[defines the dynamic semantics of bitvector slices;]{Bitvector Slices} \SemanticsRuleDef{Slice} \RenderRelation{eval_slice} @@ -162,7 +150,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \RenderProseAndFormally{eval_slice} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Lists of Bitvector Slices} +\FormalRelationsDef[defines the formal relations for lists of bitvector slices;]{Lists of Bitvector Slices} \paragraph{Syntax:} Lists of bitvector slices are grammatically derived from $\Nslices$. \paragraph{Abstract Syntax:} Lists of bitvector slices are represented by a list of $\slice$ @@ -173,13 +161,13 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \paragraph{Semantics:} Lists of bitvector slices are evaluated by $\evalslices$\\ (see \SemanticsRuleRef{Slices}). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef{Lists of Bitvector Slices} +\SyntaxDef[defines the syntax of lists of bitvector slices;]{Lists of Bitvector Slices} \begin{flalign*} \Nslices \derives \ & \Tlbracket \parsesep \ClistOne{\Nslice} \parsesep \Trbracket & \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Lists of Bitvector Slices} +\AbstractSyntaxDef[defines the abstract syntax of lists of bitvector slices;]{Lists of Bitvector Slices} \ASTRuleDef{Slices} \NotImportedToASLSpecYet{ \hypertarget{build-slices}{} @@ -201,7 +189,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef{Lists of Bitvector Slices} +\TypeRulesDef[defines the type rules for lists of bitvector slices;]{Lists of Bitvector Slices} \TypingRuleDef{Slices} \RenderRelation{annotate_slices} @@ -215,7 +203,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \RenderProseAndFormally{annotate_slices} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SemanticsRulesDef{Lists of Bitvector Slices} +\SemanticsRulesDef[defines the dynamic semantics rules for lists of bitvector slices;]{Lists of Bitvector Slices} \SemanticsRuleDef{Slices} \RenderRelation{eval_slices} diff --git a/asllib/doc/Specifications.tex b/asllib/doc/Specifications.tex index eb22e4e323..9749d44ef7 100644 --- a/asllib/doc/Specifications.tex +++ b/asllib/doc/Specifications.tex @@ -17,21 +17,9 @@ \chapter{Specifications\label{chap:Specifications}} \ASLListing{Global declarations}{TypecheckDecl}{\typingtests/TypingRule.TypecheckDecl.asl} \ChapterOutline -\begin{itemize} - \item \secref{Formal Relations for Specifications} defines the formal relations used for specifications; - \item \secref{Formal Relations for Global Declarations} defines the formal relations used for individual - global declarations; - \item \secref{Syntax of Specifications} defines the syntax of specifications; - \item \secref{Abstract Syntax of Specifications} defines the abstract syntax of specifications; - \item \secref{Typing Specifications} defines the type rules for specifications; - \item \secref{Overriding Subprograms} defines subprogram overriding and the associated type rules; - \item \secref{TopologicalOrdering} defines defined-used relations between global declarations, - which is needed to sort them; - \item \secref{Dependencies} defines how the global declarations in a specification are sorted; - \item \secref{Semantics Of Specifications} defines the dynamic semantics of specifications. -\end{itemize} -\section{Formal Relations for Specifications\label{sec:Formal Relations for Specifications}} +\SectionDef[defines the formal relations used for specifications;] + {Formal Relations for Specifications}{Formal Relations for Specifications} \hypertarget{def-specificationterm}{} \paragraph{Syntax:} Specifications are grammatically derived from $\Nspec$. @@ -41,7 +29,9 @@ \section{Formal Relations for Specifications\label{sec:Formal Relations for Spec \paragraph{Semantics:} The dynamic semantics of specifications in given by the relation $\evalspec$, which is defined in \SemanticsRuleRef{EvalSpec}. -\section{Formal Relations for Global Declarations\label{sec:Formal Relations for Global Declarations}} +\SectionDef[defines the formal relations used for individual + global declarations;] + {Formal Relations for Global Declarations}{Formal Relations for Global Declarations} Specifications are lists of global declarations. The formal relations for individual global declarations are as follows: @@ -82,14 +72,16 @@ \section{Formal Relations for Global Declarations\label{sec:Formal Relations for $\evalglobals$ and subprogram declarations are evaluated via $\evalcall$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Syntax of Specifications\label{sec:Syntax of Specifications}} +\SectionDef[defines the syntax of specifications;] + {Syntax of Specifications}{Syntax of Specifications} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{flalign*} \Nspec \derives\ & \maybeemptylist{\Ndecl} & \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Abstract Syntax of Specifications\label{sec:Abstract Syntax of Specifications}} +\SectionDef[defines the abstract syntax of specifications;] + {Abstract Syntax of Specifications}{Abstract Syntax of Specifications} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RenderType[remove_hypertargets]{spec} @@ -116,7 +108,8 @@ \section{Abstract Syntax of Specifications\label{sec:Abstract Syntax of Specific \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Typing Specifications\label{sec:Typing Specifications}} +\SectionDef[defines the type rules for specifications;] + {Typing Specifications}{Typing Specifications} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% The \untypedast{} of an ASL specification consists of a list of global declarations. @@ -311,7 +304,8 @@ \section{Typing Specifications\label{sec:Typing Specifications}} \RenderProseAndFormally{add_subprogram_decls} -\section{Overriding Subprograms\label{sec:Overriding Subprograms}} +\SectionDef[defines subprogram overriding and the associated type rules;] + {Overriding Subprograms}{Overriding Subprograms} This section defines how to override subprograms in a specification. In particular, a subprogram marked by \texttt{impdef} can be overridden by a subprogram marked by \\ \texttt{implementation}. @@ -402,7 +396,8 @@ \section{Overriding Subprograms\label{sec:Overriding Subprograms}} \RenderProseAndFormally{rename_subprograms} -\section{Defined-Used Dependencies for Global Declarations\label{sec:TopologicalOrdering}} +\SectionDef[defines defined-used relations used to sort global declarations;] + {TopologicalOrdering}{Defined-Used Dependencies for Global Declarations} This section defines how to construct a graph of \defusedependenciesterm\ between the identifiers associated with global declarations. This is achieved by associating, for each declaration $d$, the set identifiers \emph{used} by $d$, @@ -594,8 +589,8 @@ \section{Defined-Used Dependencies for Global Declarations\label{sec:Topological \RenderProseAndFormally{use_catcher} -\section{Ordering Global Declarations via Defined-Used Dependencies\label{sec:Dependencies}} - +\SectionDef[defines how the global declarations in a specification are sorted;] + {Dependencies}{Ordering Global Declarations via Defined-Used Dependencies} \begin{definition}[Strongly Connected Components] \hypertarget{relation-scc}{} Given a graph $G=(V, E)$, a \\ subset of its nodes $C \subseteq V$ is called @@ -623,7 +618,8 @@ \section{Ordering Global Declarations via Defined-Used Dependencies\label{sec:De \] \end{definition} -\section{Semantics of Specifications\label{sec:Semantics Of Specifications}} +\SectionDef[defines the dynamic semantics of specifications.] + {Semantics Of Specifications}{Semantics of Specifications} The semantics of specifications is defined via the relation $\evalspec$, which is defined next. \SemanticsRuleDef{EvalSpec} diff --git a/asllib/doc/Statements.tex b/asllib/doc/Statements.tex index 1833c21cff..7d93150eaa 100644 --- a/asllib/doc/Statements.tex +++ b/asllib/doc/Statements.tex @@ -6,30 +6,9 @@ \chapter{Statements\label{chap:Statements}} \ASLListing{Examples of statements}{Statements}{\definitiontests/Statements.asl} \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Statements} defines the formal relations used for statements; - \item \secref{PassStatements} defines pass statements; - \item \secref{AssignmentStatements} defines assignment statements; - \item \secref{SetterAssignmentStatements} defines setter assignment statements; - \item \secref{DeclarationStatements} defines declaration statements; - \item \secref{SequencingStatement} defines sequencing statements; - \item \secref{CallStatements} defines call statements; - \item \secref{ConditionalStatements} defines conditional statements; - \item \secref{CaseStatements} defines case statements; - \item \secref{AssertionStatements} defines assertion statements; - \item \secref{WhileStatements} defines while statements; - \item \secref{RepeatStatements} defines repeat statements; - \item \secref{ForStatements} defines for-looping statements; - \item \secref{ThrowStatements} defines throw statements; - \item \secref{TryStatements} defines try statements; - \item \secref{ReturnStatements} defines return statements; - \item \secref{PrintStatements} defines print statements; - \item \secref{UnreachableStatement} defines unreachable statements; - \item \secref{PragmaStatements} defines pragma statements. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Statements} +\FormalRelationsDef[defines the formal relations used for statements;]{Statements} \paragraph{Syntax:} Statements are grammatically derived from $\Nstmt$. \paragraph{Abstract Syntax:} Statements are derived in the abstract syntax from $\stmt$ @@ -51,7 +30,8 @@ \chapter{Statements\label{chap:Statements}} \RenderRelation{eval_stmt} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Pass Statements\label{sec:PassStatements}} +\SectionDef[defines pass statements;] + {PassStatements}{Pass Statements} \hypertarget{def-passstatementterm}{} \ASLListing{A \texttt{pass} statement}{semantics-spass}{\semanticstests/SemanticsRule.SPass.asl} @@ -94,7 +74,8 @@ \subsection{Semantics} \CodeSubsection{\EvalSPassBegin}{\EvalSPassEnd}{../Interpreter.ml} \hypertarget{def-assignmentstatementterm}{} -\section{Assignment Statements\label{sec:AssignmentStatements}} +\SectionDef[defines assignment statements;] + {AssignmentStatements}{Assignment Statements} \subsection{Syntax} \begin{flalign*} \Nstmt \derives \ & \Nlexpr \parsesep \Teq \parsesep \Nexpr \parsesep \Tsemicolon & @@ -179,7 +160,8 @@ \subsection{Semantics} \RenderProseAndFormally{lexpr_is_var} -\section{Setter Assignment Statements\label{sec:SetterAssignmentStatements}} +\SectionDef[defines setter assignment statements;] + {SetterAssignmentStatements}{Setter Assignment Statements} \subsection{Syntax} \begin{flalign*} \Nstmt \derives \ @@ -395,7 +377,8 @@ \subsection{Typing and semantics} As given by applying the relevant rules to the desugared AST. \hypertarget{def-declarationstatementterm}{} -\section{Declaration Statements\label{sec:DeclarationStatements}} +\SectionDef[defines declaration statements;] + {DeclarationStatements}{Declaration Statements} \subsection{Syntax} \begin{flalign*} \Nstmt \derives \ & \Nlocaldeclkeyword \parsesep \Ndeclitem \parsesep \option{\Nasty} \parsesep \Teq \parsesep \Nexpr \parsesep \Tsemicolon &\\ @@ -533,7 +516,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_stmt_SDecl} \CodeSubsection{\EvalSDeclBegin}{\EvalSDeclEnd}{../Interpreter.ml} -\section{Sequencing Statements\label{sec:SequencingStatement}} +\SectionDef[defines sequencing statements;] + {SequencingStatement}{Sequencing Statements} \hypertarget{def-sequencestatementterm}{} \ASLListing{A sequence of statements}{semantics-sseq}{\semanticstests/SemanticsRule.SSeq.asl} @@ -648,7 +632,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_stmt_SSeq} \CodeSubsection{\EvalSSeqBegin}{\EvalSSeqEnd}{../Interpreter.ml} -\section{Call Statements\label{sec:CallStatements}} +\SectionDef[defines call statements;] + {CallStatements}{Call Statements} \hypertarget{def-callstatementterm}{} Call statements are used to invoke procedures and setters. @@ -719,8 +704,8 @@ \subsection{Semantics} \hypertarget{def-conditionalstatementterm}{} -\section{Conditional Statements\label{sec:ConditionalStatements}} - +\SectionDef[defines conditional statements;] + {ConditionalStatements}{Conditional Statements} A conditional statement evaluates its \texttt{then} statement list if the condition expression evaluates to $\True$. If the condition expression evaluates to $\False$ each \texttt{elsif} condition expression is evaluated @@ -828,7 +813,8 @@ \subsection{Semantics} \CodeSubsection{\EvalSCondBegin}{\EvalSCondEnd}{../Interpreter.ml} \hypertarget{def-casestatementterm}{} -\section{Case Statements\label{sec:CaseStatements}} +\SectionDef[defines case statements;] + {CaseStatements}{Case Statements} Case statements allow executing different statements, based on which condition an expression satisfies. @@ -1201,7 +1187,8 @@ \subsection{Semantics} \ASLListing{Evaluating case alternative sub-expressions}{CaseStatement.where}{\definitiontests/CaseStatement.where.asl} \hypertarget{def-assertionstatementterm}{} -\section{Assertion Statements\label{sec:AssertionStatements}} +\SectionDef[defines assertion statements;] + {AssertionStatements}{Assertion Statements} Assertion statements are used to check that certain conditions are satisfied. They take a single \booleantypeterm{} operand, which we refer to as the \emph{condition}. If the condition is \False, the statement fails with a @@ -1267,7 +1254,8 @@ \subsection{Semantics} \CodeSubsection{\EvalSAssertBegin}{\EvalSAssertEnd}{../Interpreter.ml} -\section{While Statements\label{sec:WhileStatements}} +\SectionDef[defines while statements;] + {WhileStatements}{While Statements} \hypertarget{def-whilestatementterm}{} \ASLListing{A \texttt{while} statement}{semantics-swhile}{\semanticstests/SemanticsRule.SWhile.asl} @@ -1447,7 +1435,8 @@ \subsection{Semantics} \RenderProseAndFormally{tick_loop_limit} -\section{Repeat Statements\label{sec:RepeatStatements}} +\SectionDef[defines repeat statements;] + {RepeatStatements}{Repeat Statements} \hypertarget{def-repeatstatementterm}{} \ASLListing{A repeat statement}{semantics-srepeat}{\semanticstests/SemanticsRule.SRepeat.asl} @@ -1515,7 +1504,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_stmt_SRepeat} \CodeSubsection{\EvalSRepeatBegin}{\EvalSRepeatEnd}{../Interpreter.ml} -\section{For Statements\label{sec:ForStatements}} +\SectionDef[defines for-looping statements;] + {ForStatements}{For Statements} \hypertarget{def-forstatementterm}{} \ASLListing{\texttt{for} loops}{semantics-sfor}{\semanticstests/SemanticsRule.SFor.asl} @@ -1690,7 +1680,8 @@ \subsection{Semantics} \RenderProseAndFormally{eval_for_step} \hypertarget{def-throwstatementterm}{} -\section{Throw Statements\label{sec:ThrowStatements}} +\SectionDef[defines throw statements;] + {ThrowStatements}{Throw Statements} \subsection{Syntax} \begin{flalign*} \Nstmt \derives \ & \Tthrow \parsesep \Nexpr \parsesep \Tsemicolon & @@ -1731,7 +1722,8 @@ \subsection{Semantics} \CodeSubsection{\EvalSThrowBegin}{\EvalSThrowEnd}{../Interpreter.ml} \hypertarget{def-trystatementterm}{} -\section{Try Statements\label{sec:TryStatements}} +\SectionDef[defines try statements;] + {TryStatements}{Try Statements} \subsection{Syntax} \begin{flalign*} \Nstmt \derives \ & \Ttry \parsesep \Nstmtlist \parsesep \Tcatch \parsesep \ListOne{\Ncatcher} \parsesep \Notherwiseopt &\\ @@ -1823,7 +1815,8 @@ \subsection{Semantics} \CodeSubsection{\EvalSTryBegin}{\EvalSTryEnd}{../Interpreter.ml} \hypertarget{def-returnstatementterm}{} -\section{Return Statements\label{sec:ReturnStatements}} +\SectionDef[defines return statements;] + {ReturnStatements}{Return Statements} \subsection{Syntax} \begin{flalign*} \Nstmt \derives \ & \Treturn \parsesep \option{\Nexpr} \parsesep \Tsemicolon & @@ -1908,7 +1901,8 @@ \subsection{Semantics} \RenderProseAndFormally{write_folder} \hypertarget{def-printstatementterm}{} -\section{Print Statements\label{sec:PrintStatements}} +\SectionDef[defines print statements;] + {PrintStatements}{Print Statements} \subsection{Syntax} \begin{flalign*} \Nstmt \derives \ & \Tprint \parsesep \ClistZero{\Nexpr} \parsesep \Tsemicolon & \\ @@ -2071,7 +2065,8 @@ \subsection{Semantics} } \end{mathpar} -\section{The Unreachable Statement\label{sec:UnreachableStatement}} +\SectionDef[defines the unreachable statement;] + {UnreachableStatement}{The Unreachable Statement} \hypertarget{def-unreachablestatementterm}{} \listingref{UnreachableStatement} shows an example of using an \unreachablestatementterm{} to implement a custom form of assertion checking. @@ -2108,7 +2103,8 @@ \subsection{Abstract Syntax} \RenderProseAndFormally{eval_stmt_SUnreachable} -\section{Pragma Statements\label{sec:PragmaStatements}} +\SectionDef[defines pragma statements.] + {PragmaStatements}{Pragma Statements} \hypertarget{def-pragmastatementterm}{} \ASLListing{A pragma statement}{typing-spragma}{\typingtests/TypingRule.SPragma.asl} diff --git a/asllib/doc/SubprogramCalls.tex b/asllib/doc/SubprogramCalls.tex index 6784b2be2f..52adf51e91 100644 --- a/asllib/doc/SubprogramCalls.tex +++ b/asllib/doc/SubprogramCalls.tex @@ -15,17 +15,9 @@ \chapter{Subprogram Calls\label{chap:SubprogramCalls}} and then invoking its getter and its setter. \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Subprogram Calls} defines the formal relations for subprogram calls; - \item \SyntaxRef{Subprogram Calls} defines the syntax of subprogram calls; - \item \AbstractSyntaxRef{Subprogram Calls} defines the abstract syntax of subprogram calls; - \item \TypeRulesRef{Subprogram Calls} defines the type rules for subprogram calls, - and includes a discussion on parameter omission (\secref{ParameterOmission}); and - \item \SemanticsRulesRef{Subprogram Calls} defines the dynamic semantics of subprogram calls. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Subprogram Calls} +\FormalRelationsDef[defines the formal relations for subprogram calls;]{Subprogram Calls} \paragraph{Syntax:} Subprogram calls are grammatically derived from $\Nexpr$ and $\Nstmt$. \paragraph{Abstract Syntax:} Subprogram calls are derived in the abstract syntax by $\ECall$ and $\SCall$; @@ -33,7 +25,7 @@ \chapter{Subprogram Calls\label{chap:SubprogramCalls}} \paragraph{Semantics:} Subprogram calls are evaluated by $\evalcall$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef{Subprogram Calls} +\SyntaxDef[defines the syntax of subprogram calls;]{Subprogram Calls} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{flalign*} \Nexpr \derives\ & \Tidentifier \parsesep \PlistZero{\Nexpr} &\\ @@ -41,13 +33,14 @@ \chapter{Subprogram Calls\label{chap:SubprogramCalls}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Subprogram Calls} +\AbstractSyntaxDef[defines the abstract syntax of subprogram calls;]{Subprogram Calls} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RenderTypes[remove_hypertargets]{calls} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef{Subprogram Calls} +\TypeRulesDef[defines the type rules for subprogram calls, + and includes a discussion on parameter omission (\secref{ParameterOmission}); and]{Subprogram Calls} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% We define the following rules for annotating subprogram calls: @@ -427,7 +420,7 @@ \subsection{Parameter Omission\label{sec:ParameterOmission}} \ASLListing{Erroneous parameter omission}{ParameterOmission-bad}{\definitiontests/ParameterOmission.bad.asl} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SemanticsRulesDef{Subprogram Calls} +\SemanticsRulesDef[defines the dynamic semantics of subprogram calls.]{Subprogram Calls} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% We define the following rules for evaluating subprogram calls: diff --git a/asllib/doc/SubprogramDeclarations.tex b/asllib/doc/SubprogramDeclarations.tex index eb4b6f4aad..0b8df750e4 100644 --- a/asllib/doc/SubprogramDeclarations.tex +++ b/asllib/doc/SubprogramDeclarations.tex @@ -14,16 +14,10 @@ \chapter{Subprogram Declarations\label{chap:SubprogramDeclarations}} \ASLListing{Invoking a parametric function}{ParametricFunction2}{\definitiontests/ParametricFunction2.asl} \ChapterOutline -\begin{itemize} - \item \secref{Accessors} discusses \emph{accessors}; - \item \FormalRelationsRef{Subprogram Declarations} defines the formal relations for subprogram declarations; - \item \SyntaxRef{Subprogram Declarations} defines the syntax of subprogram declarations; - \item \AbstractSyntaxRef{Subprogram Declarations} defines the abstract syntax of subprogram declarations; and - \item \TypeRulesRef{Subprogram Declarations} defines the type rules for subprogram declarations. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Accessors\label{sec:Accessors}} +\SectionDef[discusses \emph{accessors};] + {Accessors}{Accessors} Special kinds of subprograms are \emph{getters} and \emph{setters}, which are paired to form an \emph{accessor} declaration. Intuitively, an accessor is used to abstract reading and writing to a global storage datatype. @@ -34,7 +28,7 @@ \section{Accessors\label{sec:Accessors}} \ASLListing{An accessor declaration}{AccessorDeclaration}{\definitiontests/Accessor.asl} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Subprogram Declarations} +\FormalRelationsDef[defines the formal relations for subprogram declarations;]{Subprogram Declarations} \paragraph{Syntax:} Subprogram declarations are grammatically derived from $\Ndecl$ via the subset of productions shown in \SyntaxRef{Subprogram Declarations}. @@ -46,7 +40,7 @@ \section{Accessors\label{sec:Accessors}} \paragraph{Semantics:} The dynamic semantics of subprogram calls is given in \chapref{SubprogramCalls}. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef{Subprogram Declarations} +\SyntaxDef[defines the syntax of subprogram declarations;]{Subprogram Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RequirementDef{NoEmptyBody} @@ -87,7 +81,7 @@ \section{Accessors\label{sec:Accessors}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Subprogram Declarations} +\AbstractSyntaxDef[defines the abstract syntax of subprogram declarations; and]{Subprogram Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RenderTypes[remove_hypertargets]{decl_func} @@ -619,7 +613,7 @@ \section{Accessors\label{sec:Accessors}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef{Subprogram Declarations} +\TypeRulesDef[defines the type rules for subprogram declarations.]{Subprogram Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% We define the following rules for annotating subprogram declarations: diff --git a/asllib/doc/SymbolicEquivalenceTesting.tex b/asllib/doc/SymbolicEquivalenceTesting.tex index 35810b7234..13f8c5ab01 100644 --- a/asllib/doc/SymbolicEquivalenceTesting.tex +++ b/asllib/doc/SymbolicEquivalenceTesting.tex @@ -25,13 +25,9 @@ \chapter{Symbolic Reduction and Equivalence Testing\label{chap:SymbolicEquivalen desired form varies according to the functions utilising this value). \ChapterOutline -\begin{itemize} - \item \secref{Equivalence Definitions} formally defines equivalence for expressions, types, constraints, and bitfields; - \item \secref{symbolicexpressions} defines \symbolicexpressionsterm{} and operations over \symbolicexpressionsterm{}; and - \item \secref{SymbolicReductionAndEquivalenceTestingRules} defines rules for symbolic reduction and equivalence testing. -\end{itemize} -\section{Equivalence Definitions\label{sec:Equivalence Definitions}} +\SectionDef[formally defines equivalence for expressions, types, constraints, and bitfields;] + {Equivalence Definitions}{Equivalence Definitions} \begin{definition}[Expression Equivalence] \hypertarget{def-equivalentexprsterm}{} We say that $\veone$ and $\vetwo$ are \emph{\equivalentexprsterm{}} in the \staticenvironmentterm{} $\tenv$ @@ -68,7 +64,8 @@ \section{Equivalence Definitions\label{sec:Equivalence Definitions}} and type equivalence ($\typeequal$) are replaced by their respective definitions above. -\section{Symbolic Expressions\label{sec:symbolicexpressions}} +\SectionDef[defines \symbolicexpressionsterm{} and operations over \symbolicexpressionsterm{}; and] + {symbolicexpressions}{Symbolic Expressions} \hypertarget{def-symbolicexpressionterm}{} Our symbolic reduction and equivalence testing rules employ \emph{\symbolicexpressionsterm}, defined below: \RenderTypes{symbolic_expressions} @@ -268,7 +265,8 @@ \section{Symbolic Expressions\label{sec:symbolicexpressions}} \alpha(\polynomialdividebyterm(\vpone, \vm, 0)) = \CannotBeTransformed \enspace. \] -\section{Typing Rules\label{sec:SymbolicReductionAndEquivalenceTestingRules}} +\SectionDef[defines rules for symbolic reduction and equivalence testing.] + {SymbolicReductionAndEquivalenceTestingRules}{Symbolic Reduction and Equivalence Testing Rules} We employ the following rules: \begin{TypingRuleList}{SymbolicEquivalenceTesting} diff --git a/asllib/doc/SymbolicSubsumptionTesting.tex b/asllib/doc/SymbolicSubsumptionTesting.tex index 350682deb8..19c751d4e0 100644 --- a/asllib/doc/SymbolicSubsumptionTesting.tex +++ b/asllib/doc/SymbolicSubsumptionTesting.tex @@ -84,13 +84,9 @@ \chapter{Symbolic Domain Subset Testing\label{chap:SymbolicDomainSubsetTesting}} that we refer to as \emph{symbolic domains} and then checking subsumption over the symbolic domains. \ChapterOutline -\begin{itemize} - \item \secref{Symbolic Domains} defines a symbolic representation for sets of integers; and - \item \secref{Symbolic Reasoning} defines the symbolic reasoning used for domain subset - testing. -\end{itemize} -\section{Symbolic Domains\label{sec:Symbolic Domains}} +\SectionDef[defines a symbolic representation for sets of integers; and] + {Symbolic Domains}{Symbolic Domains} \hypertarget{def-symbolicdomain}{} We define the \emph{symbolic domain} datatype, reusing $\intconstraint$ from the untyped AST, @@ -108,8 +104,9 @@ \section{Symbolic Domains\label{sec:Symbolic Domains}} which represents the set of all integers. \end{itemize} -\section{Symbolic Reasoning\label{sec:Symbolic Reasoning}} - +\SectionDef[defines the symbolic reasoning used for domain subset + testing.] + {Symbolic Reasoning}{Symbolic Reasoning} We define the following rules for symbolic subsumption testing: \begin{TypingRuleList}{SymbolicSubsumptionTesting} diff --git a/asllib/doc/Syntax.tex b/asllib/doc/Syntax.tex index 62a928cb13..df7599cb81 100644 --- a/asllib/doc/Syntax.tex +++ b/asllib/doc/Syntax.tex @@ -96,20 +96,9 @@ \section*{Resolving ambiguities: conflicts, token priorities, and associativitie \end{itemize} \ChapterOutline -\begin{itemize} - \item \secref{InlinedDerivations} defines \emph{inlined derivations}; - \item \secref{ParametricProductions} defines \emph{parametric productions}; - \item \secref{ASLParametricProductions} introduces the parametric productions - used for the ASL grammar; - \item \secref{ASLGrammar} defines the ASL grammar; - \item \secref{ParseTrees} defines parse trees; - \item \secref{PriorityAndAssociativity} defines the priority and associativity - of tokens; and - \item \secref{GrammarExamples} presents examples showing how the grammar and - the priority and associativity rules are used to parse ASL text. -\end{itemize} -\section{Inlined Derivations\label{sec:InlinedDerivations}} +\SectionDef[defines \emph{inlined derivations};] + {InlinedDerivations}{Inlined Derivations} Context-free grammars consist of a list of \emph{derivations} $N \derives \KleeneStar{S}$ where $N$ is a non-terminal symbol and $S$ is a list of non-terminal symbols and terminal symbols, which correspond to tokens. @@ -160,7 +149,8 @@ \section{Inlined Derivations\label{sec:InlinedDerivations}} Barring mutually-recursive derivations involving inlined derivations, it is possible to expand all inlined derivations to obtain a context-free grammar without any inlined derivations. -\section{Parametric Productions\label{sec:ParametricProductions}} +\SectionDef[defines \emph{parametric productions};] + {ParametricProductions}{Parametric Productions} A parametric production has the form $N(p_{1..m}) \derives R_1 \;|\; \ldots \;|\; R_k$ where $p_{1..m}$ are place holders for grammar symbols and may appear in any of the alternatives $R_{1..k}$. @@ -201,7 +191,9 @@ \section{Parametric Productions\label{sec:ParametricProductions}} \Nspec \derives\ & \Ndecllist & \end{flalign*} -\section{ASL Parametric Productions\label{sec:ASLParametricProductions}} +\SectionDef[introduces the parametric productions + used for the ASL grammar;] + {ASLParametricProductions}{ASL Parametric Productions} We define the following parametric productions for various types of lists and optional productions. \paragraph{Optional Symbol} @@ -265,7 +257,8 @@ \section{ASL Parametric Productions\label{sec:ASLParametricProductions}} \TClistZero{x} \derives \ & \option{\TClistOne{x}} &\\ \end{flalign*} -\section{ASL Grammar\label{sec:ASLGrammar}} +\SectionDef[defines the ASL grammar;] + {ASLGrammar}{ASL Grammar} We now present the list of derivations for the ASL Grammar where the start non-terminal is $\Nspec$. % The derivations allow certain parse trees where lists may have invalid sizes. @@ -684,7 +677,8 @@ \section{ASL Grammar\label{sec:ASLGrammar}} |\ & \Tor \;|\; \Trdiv \;|\; \Tshl \;|\; \Tshr \;|\; \Tpow \;|\; \Tcoloncolon \;|\; \Tplusplus \end{flalign*} -\section{Parse Trees\label{sec:ParseTrees}} +\SectionDef[defines parse trees;] + {ParseTrees}{Parse Trees} We now define \emph{parse trees} for the ASL expanded grammar. Those are later used to build Abstract Syntax Trees. \begin{definition}[Parse Trees] @@ -755,7 +749,9 @@ \section{Parse Trees\label{sec:ParseTrees}} \Lang{G} = \{\yield(n) \;|\; n \text{ is a well-formed parse tree for }G\} \enspace. \] -\section{Priority and Associativity for Parsing Tokens\label{sec:PriorityAndAssociativity}} +\SectionDef[defines the priority and associativity + of tokens; and] + {PriorityAndAssociativity}{Priority and Associativity for Parsing Tokens} As described in the introduction to \chapref{Syntax}, tokens that may cause a \shiftreduceconflictterm{} are assigned a priority, and each priority is assigned an associativity. Tokens that cannot cause \shiftreduceconflictsterm{} @@ -796,8 +792,9 @@ \section{Priority and Associativity for Parsing Tokens\label{sec:PriorityAndAsso \end{center} -\section{Grammar Examples\label{sec:GrammarExamples}} - +\SectionDef[presents examples showing how the grammar and + the priority and associativity rules are used to parse ASL text.] + {GrammarExamples}{Grammar Examples} \ExampleDef{Derivation of a Valid Expression} The expression \texttt{1 + 3} is transformed by the lexical analysis into: diff --git a/asllib/doc/TopLevel.tex b/asllib/doc/TopLevel.tex index 8edcecf3a5..cab81d9c5b 100644 --- a/asllib/doc/TopLevel.tex +++ b/asllib/doc/TopLevel.tex @@ -16,17 +16,9 @@ \chapter{Top Level\label{chap:TopLevel}} replaced with a translation to a hardware description language. \ChapterOutline -\begin{itemize} - \item \secref{Example Interpreter} presents an example of how to construct an ASL interpreter; - \item \secref{Renaming Local Storage Elements in the Standard Library} explains how local storage - elements of the standard library can be renamed to allow them to be correctly combined into - arbitrary specifications; - \item \secref{Marking Standard Library Functions} defines how to mark subprograms in the standard - library to allow distinguishing them from other subprograms. -\end{itemize} - -\section{Example Interpreter\label{sec:Example Interpreter}} +\SectionDef[presents an example of how to construct an ASL interpreter;] + {Example Interpreter}{Example Interpreter} \NotImportedToASLSpecYet{ \hypertarget{def-checkandinterpret}{} The relation @@ -100,7 +92,10 @@ \subsubsection{TopLevelRule.CheckAndInterpret\label{sec:TopLevelRule.CheckAndInt %% Beginning of rename locals-related functions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Renaming Local Storage Elements in the Standard Library\label{sec:Renaming Local Storage Elements in the Standard Library}} +\SectionDef[explains how local storage + elements of the standard library can be renamed to allow them to be correctly combined into + arbitrary specifications;] + {Renaming Local Storage Elements in the Standard Library}{Renaming Local Storage Elements in the Standard Library} % Transliteration comment: this transformation only applies to untyped AST node types. In order to combine the standard library declarations with a given specification, @@ -1564,8 +1559,9 @@ \section{Renaming Local Storage Elements in the Standard Library\label{sec:Renam %% End of rename locals-related functions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Marking Standard Library Functions\label{sec:Marking Standard Library Functions}} - +\SectionDef[defines how to mark subprograms in the standard + library to allow distinguishing them from other subprograms.] + {Marking Standard Library Functions}{Marking Standard Library Functions} \ASTRuleDef{SetBuiltin} \NotImportedToASLSpecYet{ \hypertarget{def-setbuiltin}{} diff --git a/asllib/doc/TypeAttributes.tex b/asllib/doc/TypeAttributes.tex index 9adf5a6307..e932c79b3c 100644 --- a/asllib/doc/TypeAttributes.tex +++ b/asllib/doc/TypeAttributes.tex @@ -1,5 +1,6 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Basic Type Attributes\label{sec:BasicTypeAttributes}} +\SectionDef[defines predicates for classifying types and functions for inspecting their structure;] + {BasicTypeAttributes}{Basic Type Attributes} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% This section defines some basic predicates for classifying types as well as diff --git a/asllib/doc/TypeChecking.tex b/asllib/doc/TypeChecking.tex index 9af950adfe..fd6f5ab656 100644 --- a/asllib/doc/TypeChecking.tex +++ b/asllib/doc/TypeChecking.tex @@ -43,12 +43,9 @@ \chapter{Type System Definitions\label{chap:TypeChecking}} Throughout this document we use $\tty$ to denote a type variable, which should not be confused with the abstract syntax variable $\ty$. \ChapterOutline -\begin{itemize} - \item \secref{StaticEnvironments} defines static environments; and - \item \secref{Typing Rule Configurations} defines the configurations used in typing rules. -\end{itemize} -\section{Static Environments\label{sec:StaticEnvironments}} +\SectionDef[defines static environments; and] + {StaticEnvironments}{Static Environments} A \emph{\staticenvironmentterm{}} (also called a \emph{type environment}) is what the typing rules operate over: a structure, which amongst other things, associates types to variables. Intuitively, the typing of a specification makes an initial environment evolve, with new types as given by the @@ -123,7 +120,8 @@ \section{Static Environments\label{sec:StaticEnvironments}} \] \end{definition} -\section{Typing Rule Configurations\label{sec:Typing Rule Configurations}} +\SectionDef[defines the configurations used in typing rules.] + {Typing Rule Configurations}{Typing Rule Configurations} The output configurations of type system assertions have two flavours: \begin{description} \item[Normal Outputs.] diff --git a/asllib/doc/TypeDeclarations.tex b/asllib/doc/TypeDeclarations.tex index 53f9ecd818..3048d7e843 100644 --- a/asllib/doc/TypeDeclarations.tex +++ b/asllib/doc/TypeDeclarations.tex @@ -5,15 +5,9 @@ \chapter{Type Declarations\label{chap:TypeDeclarations}} See \ExampleRef{Types} for examples of type declarations. \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Type Declarations} defines the formal relations for type declarations; - \item \SyntaxRef{Type Declarations} defines the syntax for type declarations; - \item \AbstractSyntaxRef{Type Declarations} defines the abstract syntax for type declarations; - \item \TypeRulesRef{Type Declarations} defines the type rules for type declarations. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Type Declarations} +\FormalRelationsDef[defines the formal relations for type declarations;]{Type Declarations} \paragraph{Syntax:} Type declarations are grammatically derived from $\Ndecl$. \paragraph{Abstract Syntax:} Type declarations are derived in the abstract syntax from $\decl$, and generated by $\builddecl$ (see \ASTRuleRef{TypeDecl}). @@ -21,7 +15,7 @@ \chapter{Type Declarations\label{chap:TypeDeclarations}} \paragraph{Semantics:} Type declarations have no associated dynamic semantics. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef{Type Declarations} +\SyntaxDef[defines the syntax for type declarations;]{Type Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{flalign*} \Ndecl \derives \ & \Ttype \parsesep \Tidentifier \parsesep \Tof \parsesep \Ntydecl \parsesep \Tsemicolon&\\ @@ -32,7 +26,7 @@ \chapter{Type Declarations\label{chap:TypeDeclarations}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Type Declarations} +\AbstractSyntaxDef[defines the abstract syntax for type declarations;]{Type Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RenderTypes[remove_hypertargets]{decl_type} @@ -82,7 +76,7 @@ \chapter{Type Declarations\label{chap:TypeDeclarations}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef{Type Declarations} +\TypeRulesDef[defines the type rules for type declarations.]{Type Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% We define the following rules for annotating type declarations: \begin{TypingRuleList}{TypeDeclarations} diff --git a/asllib/doc/TypeDomains.tex b/asllib/doc/TypeDomains.tex index 0a6e0d01be..fb04727852 100644 --- a/asllib/doc/TypeDomains.tex +++ b/asllib/doc/TypeDomains.tex @@ -1,5 +1,6 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Domain of Values for Types\label{sec:DomainOfValuesForTypes}} +\SectionDef[defines the semantics of types by associating a value to each type;] + {DomainOfValuesForTypes}{Domain of Values for Types} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% This section formalises the concept of the set of values for a given type. The formalism is given in the form of inference rules, although those are not meant diff --git a/asllib/doc/TypeSystemUtilities.tex b/asllib/doc/TypeSystemUtilities.tex index 2b175d801b..352df50665 100644 --- a/asllib/doc/TypeSystemUtilities.tex +++ b/asllib/doc/TypeSystemUtilities.tex @@ -2,7 +2,6 @@ \chapter{Type System Utility Rules\label{chap:TypeSystemUtilityRules}} This chapter defines functions and relations used by the type system. -\ChapterOutline \begin{TypingRuleList}{TypeSystemUtilities} \TypingRuleDef[checks that a list contains no duplicate elements.]{CheckNoDuplicates} diff --git a/asllib/doc/Types.tex b/asllib/doc/Types.tex index bb4d2cb9e2..048020663b 100644 --- a/asllib/doc/Types.tex +++ b/asllib/doc/Types.tex @@ -12,36 +12,9 @@ \chapter{Types\label{chap:Types}} \ASLListing{Examples of Types}{Types}{\definitiontests/Types.asl} \ChapterOutline -\begin{itemize} - \item \FormalRelationsRef{Types} defines the formal relations for types; - \item \AbstractSyntaxRef{Types} defines how the abstract syntax nodes for types - are generated; - \item \secref{IntegerTypes} defines the \integertypeterm{}; - \item \secref{RealType} defines the \realtypeterm{}; - \item \secref{StringType} defines the \stringtypeterm{}; - \item \secref{BooleanType} defines the \booleantypeterm{}; - \item \secref{BitvectorTypes} defines the \bitvectortypeterm{}; - \item \secref{TupleTypes} defines \Tupletypesterm{}; - \item \secref{ParenthesisedTypes} defines parenthesised types; - \item \secref{EnumerationTypes} defines \Enumerationtypesterm{}; - \item \secref{ArrayTypes} defines array types; - \item \secref{RecordTypes} defines record types; - \item \secref{ExceptionTypes} defines exception types; - \item \secref{CollectionTypes} defines collection types; - \item \secref{NamedTypes} defines named types; - \item \secref{DeclaredTypes} defines \emph{declared types} and restrictions over them; - \item \secref{DomainOfValuesForTypes} defines the semantics of types by associating a value to each type; - \item \secref{BasicTypeAttributes} assigns basic properties to types, which are useful - in classifying them; - \item \secref{RelationsOnTypes} defines relations on types that are needed to typecheck - expressions and statements; and - \item \secref{BaseValues} defines how to generate a \emph{base value} --- an expression - to initialise a storage element of a given type for which no initialising - expression is given. -\end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef{Types} +\FormalRelationsDef[defines the formal relations for types;]{Types} \paragraph{Syntax:} \Anonymoustypes{} are grammatically derived from $\Nty$ and types that must be declared and named are grammatically derived from $\Ntydecl$; @@ -59,7 +32,8 @@ \chapter{Types\label{chap:Types}} (see \SemanticsRuleRef{ATC} and \SemanticsRuleRef{IsValOfType}). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef{Types} +\AbstractSyntaxDef[defines how the abstract syntax nodes for types + are generated;]{Types} \NotImportedToASLSpecYet{ \hypertarget{build-ty}{} The function @@ -124,7 +98,8 @@ \chapter{Types\label{chap:Types}} \end{mathpar} \hypertarget{integertypeterm}{} -\section{Integer Types\label{sec:IntegerTypes}} +\SectionDef[defines the \integertypeterm{};] + {IntegerTypes}{Integer Types} The \emph{\integertypesterm{}} represent the mathematical integer values. There are four kinds of integer types, and we @@ -369,7 +344,8 @@ \subsection{Typing Integer Types\label{sec:TypingIntegerTypes}} \RenderProseAndFormally{annotate_constraint} -\section{The Real Type\label{sec:RealType}} +\SectionDef[defines the \realtypeterm{};] + {RealType}{The Real Type} \hypertarget{realtypeterm}{} The \emph{\realtypeterm{}} represents mathematical rational number values. There is no bound on the minimum and maximum rational value that can be represented, @@ -412,7 +388,8 @@ \subsection{Typing the Real Type\label{sec:TypingRealType}} \RenderProseAndFormally{annotate_type_t_real} \CodeSubsection{\TRealBegin}{\TRealEnd}{../Typing.ml} -\section{The String Type\label{sec:StringType}} +\SectionDef[defines the \stringtypeterm{};] + {StringType}{The String Type} \hypertarget{stringtypeterm}{} \hypertarget{stringtypesterm}{} The \emph{\stringtypeterm{}} represents strings of characters. @@ -451,7 +428,8 @@ \subsection{Typing the String Type\label{sec:TypingStringType}} \RenderProseAndFormally{annotate_type_t_string} \CodeSubsection{\TStringBegin}{\TStringEnd}{../Typing.ml} -\section{The Boolean Type\label{sec:BooleanType}} +\SectionDef[defines the \booleantypeterm{};] + {BooleanType}{The Boolean Type} \hypertarget{booleantypeterm}{} The \emph{\booleantypeterm{}} represents Booleans. @@ -484,7 +462,8 @@ \subsection{Typing the Boolean Type\label{sec:TypingBooleanType}} \RenderProseAndFormally{annotate_type_t_bool} \CodeSubsection{\TBoolBegin}{\TBoolEnd}{../Typing.ml} -\section{Bitvector Types\label{sec:BitvectorTypes}} +\SectionDef[defines the \bitvectortypeterm{};] + {BitvectorTypes}{Bitvector Types} \hypertarget{bitvectortypeterm}{} \emph{Bitvectors} represent sequences of $0$ and $1$ bits ordered according to \RequirementRef{BitvectorOrdering}. % @@ -623,7 +602,8 @@ \subsection{Typing Bitvector Types} \RenderProseAndFormally{annotate_type_t_bits} \CodeSubsection{\TBitsBegin}{\TBitsEnd}{../Typing.ml} -\section{Tuple Types\label{sec:TupleTypes}} +\SectionDef[defines \Tupletypesterm{};] + {TupleTypes}{Tuple Types} \hypertarget{tupletypeterm}{} Types can be combined into \tupletypesterm{} whose values consist of tuples of values of those types. @@ -691,7 +671,8 @@ \subsection{Typing Tuple Types\label{sec:TypingTupleTypes}} \RenderProseAndFormally{annotate_type_t_tuple} \CodeSubsection{\TTupleBegin}{\TTupleEnd}{../Typing.ml} -\section{Parenthesised Types\label{sec:ParenthesisedTypes}} +\SectionDef[defines parenthesised types;] + {ParenthesisedTypes}{Parenthesised Types} A single type inside parentheses is not considered to be a tuple, but rather the element inside the parenthesis. Parenthesising a type can be used to improve readability. @@ -716,7 +697,8 @@ \subsection{Abstract Syntax} } \end{mathpar} -\section{Enumeration Types\label{sec:EnumerationTypes}} +\SectionDef[defines \Enumerationtypesterm{};] + {EnumerationTypes}{Enumeration Types} \hypertarget{enumerationtypeterm}{} The \emph{\enumerationtypeterm} defines a list of enumeration literals, also referred to as \emph{labels}, that act @@ -790,7 +772,8 @@ \subsection{Typing Enumeration Types\label{sec:TypingEnumerationTypes}} \RenderProseAndFormally{annotate_type_t_enum_decl} \CodeSubsection{\TEnumDeclBegin}{\TEnumDeclEnd}{../Typing.ml} -\section{Array Types\label{sec:ArrayTypes}} +\SectionDef[defines array types;] + {ArrayTypes}{Array Types} \hypertarget{arraytypeterm}{} % Arrays are sequences of values of a single given type. @@ -884,7 +867,8 @@ \subsection{Typing Array Types\label{sec:TypingArrayTypes}} \RenderProseAndFormally{check_underlying_integer} \CodeSubsection{\CheckUnderlyingIntegerBegin}{\CheckUnderlyingIntegerEnd}{../Typing.ml} -\section{Record Types\label{sec:RecordTypes}} +\SectionDef[defines record types;] + {RecordTypes}{Record Types} \hypertarget{recordtypeterm}{} % A record is a \structuredtypeterm{} consisting of a list of field identifiers which denote individual storage elements. @@ -924,7 +908,8 @@ \subsection{Typing Record Types\label{sec:TypingRecordTypes}} \RenderProseAndFormally{annotate_type_t_record_exception} \CodeSubsection{\TStructuredDeclBegin}{\TStructuredDeclEnd}{../Typing.ml} -\section{Exception Types\label{sec:ExceptionTypes}} +\SectionDef[defines exception types;] + {ExceptionTypes}{Exception Types} \hypertarget{exceptiontypeterm}{} An exception is a \structuredtypeterm{} consisting of a list of field identifiers which denote individual storage elements. @@ -962,7 +947,8 @@ \subsection{Abstract Syntax} \subsection{Typing Exception Types} The rule for typing exception types is \TypingRuleRef{TStructuredDecl}. -\section{Collection Types\label{sec:CollectionTypes}} +\SectionDef[defines collection types;] + {CollectionTypes}{Collection Types} \hypertarget{collectiontypeterm}{} \ASLListing{Collection types}{TCollection}{\typingtests/TypingRule.TCollection.asl} @@ -1011,7 +997,8 @@ \subsection{Typing Collection Types} \RenderProseAndFormally{annotate_type_t_collection} -\section{Named Types\label{sec:NamedTypes}} +\SectionDef[defines named types;] + {NamedTypes}{Named Types} A named type declaration allows declaring a new type associated with the given name. The intent is that, by default, any named type should not be assignable to or from any other named type, even if they coincidentally have the same \structureterm. @@ -1069,7 +1056,8 @@ \subsection{Typing Named Types\label{sec:TypingNamedTypes}} \RenderProseAndFormally{annotate_type_t_named} \CodeSubsection{\TNamedBegin}{\TNamedEnd}{../Typing.ml} -\section{Declared Types\label{sec:DeclaredTypes}} +\SectionDef[defines \emph{declared types} and restrictions over them;] + {DeclaredTypes}{Declared Types} A declared type can be an \enumerationtypeterm{}, a \recordtypeterm, an \exceptiontypeterm, or an \anonymoustype. \subsection{Syntax} \begin{flalign*} diff --git a/asllib/doc/dictionary.txt b/asllib/doc/dictionary.txt index 690bd09928..193619b4d5 100644 --- a/asllib/doc/dictionary.txt +++ b/asllib/doc/dictionary.txt @@ -188,6 +188,7 @@ attempt attempted attempting attempts +attributes authoritative automatically auxiliary @@ -2129,6 +2130,7 @@ sugar sum summarised summarises +summary summation summing sums diff --git a/asllib/doc/doclint.py b/asllib/doc/doclint.py index cfdb0827b6..c8b27c414e 100755 --- a/asllib/doc/doclint.py +++ b/asllib/doc/doclint.py @@ -889,6 +889,9 @@ def spellcheck(reference_dictionary_path: str, latex_files: list[str]) -> int: r"\\end{(?:AST|Typing|Semantics)RuleList}", r"\\TypingRuleRef{.*?}", r"\\TypingRuleDef(?:\[.*?\])?{.*?}", + # Ignore the optional outline description and stable label, while + # leaving the displayed section title to be spellchecked. + r"\\(?:SectionDef|OutlineSubsectionDef)(?:\[.*?\])?\s*{.*?}", r"\\SemanticsRuleRef{.*?}", r"\\SemanticsRuleDef(?:\[.*?\])?{.*?}", r"\\RequirementDef{.*?}", diff --git a/asllib/doc/macros.hva b/asllib/doc/macros.hva index 021cc5e5f6..855a5d7352 100644 --- a/asllib/doc/macros.hva +++ b/asllib/doc/macros.hva @@ -133,6 +133,75 @@ \let\ASLRecordTypingRule\my@ASLRecordTypingRule \let\ASLRecordSemanticsRule\my@ASLRecordSemanticsRule} +% Chapter outlines use the LaTeX aux file in the PDF build. Record the same +% information in HeVeA's .haux file for HTML. Number outlines by their order +% in the document: this avoids relying on LaTeX's internal chapter counter, +% which HeVeA does not provide, while still allowing a chapter to span files. +\newcounter{ASLChapterOutlineIndex} +\let\my@ASLCurrentOutlineSection\@empty + +\newcommand{\my@ASLChapterOutlineWrite}[3]{% + \@auxdowrite{\@print{\ASLChapterOutlineEntry}\{#1\}\{#2\}\{\@subst{#3}\}\@print{ +}}} + +\newcommand{\my@ASLChapterOutlineSubwrite}[4]{% + \@auxdowrite{\@print{\ASLChapterOutlineSubentry}\{#1\}\{#2\}\{#3\}\{\@subst{#4}\}\@print{ +}}} + +\newcommand{\my@ASLChapterOutlineEntry}[3]{% + \@ifundefined{ASLChapterOutline@#1}{% + \newtokens{\csname ASLChapterOutline@#1\endcsname}% + }{}% + \addtokens{\csname ASLChapterOutline@#1\endcsname} + {\ASLChapterOutlineSection{#1}{#2}{#3}}} + +\newcommand{\my@ASLChapterOutlineSubentry}[4]{% + \@ifundefined{ASLChapterOutlineSubsections@#1@#2}{% + \newtokens{\csname ASLChapterOutlineSubsections@#1@#2\endcsname}% + }{}% + \addtokens{\csname ASLChapterOutlineSubsections@#1@#2\endcsname} + {\item \secref{#3} #4}} + +\newcommand{\my@ASLChapterOutlineSection}[3]{% + \item \secref{#2} #3% + \@ifundefined{ASLChapterOutlineSubsections@#1@#2}{}{% + \begin{itemize}% + \csname ASLChapterOutlineSubsections@#1@#2\endcsname + \end{itemize}}} + +\newcommand{\my@ChapterOutline}{% + \stepcounter{ASLChapterOutlineIndex}% + \global\let\my@ASLCurrentOutlineSection\@empty + \paragraph{Outline} The rest of this chapter is organized as follows: + \begin{itemize}% + \@ifundefined{ASLChapterOutline@\arabic{ASLChapterOutlineIndex}}{% + \item \emph{Run HeVeA again to generate this chapter outline.}% + }{% + \csname ASLChapterOutline@\arabic{ASLChapterOutlineIndex}\endcsname + }% + \end{itemize}} + +\newcommand{\my@SectionDef}[3][]{% + \section{#3\label{sec:#2}}% + \gdef\my@ASLCurrentOutlineSection{#2}% + \my@ASLChapterOutlineWrite{\arabic{ASLChapterOutlineIndex}}{#2}{#1}} + +\newcommand{\my@OutlineSubsectionDef}[3][]{% + \subsection{#3\label{sec:#2}}% + \my@ASLChapterOutlineSubwrite + {\arabic{ASLChapterOutlineIndex}}{\my@ASLCurrentOutlineSection}{#2}{#1}} + +% HeVeA reads .haux from an earlier AtBeginDocument hook. Stored entries must +% therefore see these definitions before the document-level overrides below. +\addrevtokens{\@atbegindocument} + {\let\ASLChapterOutlineEntry\my@ASLChapterOutlineEntry + \let\ASLChapterOutlineSubentry\my@ASLChapterOutlineSubentry} +\AtBeginDocument + {\let\ASLChapterOutlineSection\my@ASLChapterOutlineSection + \let\ChapterOutline\my@ChapterOutline + \let\SectionDef\my@SectionDef + \let\OutlineSubsectionDef\my@OutlineSubsectionDef} + % Some hyperlinked math constructs produce tables in display mode. Put the link % inside the display-mode construct there, and around the compact inline % construct otherwise, to avoid invalid HTML. From 00f8e71999769795796e020532b6002f9f3f5e19 Mon Sep 17 00:00:00 2001 From: Roman-Manevich Date: Tue, 4 Aug 2026 21:51:05 +0100 Subject: [PATCH 2/2] [asl reference] addressing review comments --- asllib/doc/ASLFormal.tex | 10 ++--- asllib/doc/ASLmacros.tex | 10 ++--- asllib/doc/AbstractSyntax.tex | 52 +++++++++++------------ asllib/doc/AssignableExpressions.tex | 16 +++---- asllib/doc/Bitfields.tex | 8 ++-- asllib/doc/BlockStatements.tex | 2 +- asllib/doc/CatchingExceptions.tex | 8 ++-- asllib/doc/ErrorCodes.tex | 8 ++-- asllib/doc/Expressions.tex | 38 ++++++++--------- asllib/doc/GlobalPragmas.tex | 4 +- asllib/doc/GlobalStorageDeclarations.tex | 6 +-- asllib/doc/Literals.tex | 6 +-- asllib/doc/LocalStorageDeclarations.tex | 12 +++--- asllib/doc/PatternMatching.tex | 14 +++--- asllib/doc/PrimitiveOperations.tex | 12 +++--- asllib/doc/Semantics.tex | 4 +- asllib/doc/SideEffects.tex | 2 +- asllib/doc/Slicing.tex | 20 ++++----- asllib/doc/Specifications.tex | 14 +++--- asllib/doc/Statements.tex | 36 ++++++++-------- asllib/doc/SubprogramCalls.tex | 6 +-- asllib/doc/SubprogramDeclarations.tex | 6 +-- asllib/doc/SymbolicEquivalenceTesting.tex | 2 +- asllib/doc/Syntax.tex | 8 ++-- asllib/doc/TopLevel.tex | 2 +- asllib/doc/TypeAttributes.tex | 2 +- asllib/doc/TypeDeclarations.tex | 6 +-- asllib/doc/TypeDomains.tex | 2 +- asllib/doc/Types.tex | 30 ++++++------- asllib/doc/macros.hva | 4 +- 30 files changed, 174 insertions(+), 176 deletions(-) diff --git a/asllib/doc/ASLFormal.tex b/asllib/doc/ASLFormal.tex index fbc2fe1dcb..f2ed09beea 100644 --- a/asllib/doc/ASLFormal.tex +++ b/asllib/doc/ASLFormal.tex @@ -5,7 +5,7 @@ \chapter{Formal System \label{chap:FormalSystem}} \ChapterOutline -\SectionDef[defines general mathematical concepts and notations;] +\SectionDef[defines general mathematical concepts and notations] {Mathematical Definitions and Notations}{Mathematical Definitions and Notations} \hypertarget{def-triangleq}{} We use $\triangleq$ to define mathematical concepts. @@ -501,7 +501,7 @@ \subsection{OCaml-style Notations} \end{definition} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SectionDef[defines the concept of \emph{inference rules};] +\SectionDef[defines the concept of \emph{inference rules}] {Inference Rules}{Inference Rules} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \hypertarget{def-inferencerule}{} @@ -670,7 +670,7 @@ \subsection{OCaml-style Notations} for a given transition. \hypertarget{def-configuration}{} -\SectionDef[introduces \emph{\configurationsterm{}} as a way of representing compound data;] +\SectionDef[introduces \emph{\configurationsterm{}} as a way of representing compound data] {Configurations}{Configurations} Our relations range over compound values. That is, values that often nest tuples and lists inside other tuples and lists. We refer to such values as \emph{\configurationsterm}. To make it easier to distinguish between different \configurationsterm{}, @@ -785,7 +785,7 @@ \subsection{OCaml-style Notations} \end{mathpar} \end{description} -\SectionDef[introduces AST-related notations that are used in inference rules;] +\SectionDef[introduces AST-related notations that are used in inference rules] {ASTNotations}{AST-related Notations} When deconstructing AST record nodes such as $\{f_1:t_1,\ldots,f_k:t_k\}$, we sometimes only care about a subset of the fields $\{f_{i_1},\ldots,f_{i_m}\} \subset \{f_{1..k}\}$. @@ -850,7 +850,7 @@ \subsection{OCaml-style Notations} which are components of the previously assigned variables $\vmone$ and $\vmtwo$. \hypertarget{def-shortcircuitrulemacro}{} -\SectionDef[defines rule macros, which compactly represent multiple rules;] +\SectionDef[defines rule macros, which compactly represent multiple rules] {ShortCircuitRuleMacros}{Short-circuit Rule Macros} \emph{\Shortcircuitrulemacros}, or \emph{rule macros}, for short, allow us to succinctly define sets of rules. Specifically, they allow us to capture situations where diff --git a/asllib/doc/ASLmacros.tex b/asllib/doc/ASLmacros.tex index 7e024ba61d..5e5d56bbf8 100644 --- a/asllib/doc/ASLmacros.tex +++ b/asllib/doc/ASLmacros.tex @@ -170,13 +170,11 @@ \newcommand\NotImportedToASLSpecYet[1]{#1} \newcommand\FormalRelationsDef[2][]{\SectionDef[#1]{Formal Relations for #2}{Formal Relations for #2}} -\newcommand\FormalRelationsRef[1]{\secref{Formal Relations for #1}} % DO NOT LINT: public convenience macro. \newcommand\SyntaxDef[2][]{\SectionDef[#1]{Syntax of #2}{Syntax of #2}} \newcommand\SyntaxRef[1]{\secref{Syntax of #1}} \newcommand\AbstractSyntaxDef[2][]{\SectionDef[#1]{Abstract Syntax of #2}{Abstract Syntax of #2}} \newcommand\AbstractSyntaxRef[1]{\secref{Abstract Syntax of #1}} \newcommand\TypeRulesDef[2][]{\SectionDef[#1]{Type Rules for #2}{Type Rules for #2}} -\newcommand\TypeRulesRef[1]{\secref{Type Rules for #1}} % DO NOT LINT: public convenience macro. \newcommand\SemanticsRulesDef[2][]{\SectionDef[#1]{Dynamic Semantics Rules for #2}{Dynamic Semantics Rules for #2}} \newcommand\SemanticsRulesRef[1]{\secref{Dynamic Semantics Rules for #1}} \newcommand\textfunc[1]{\textit{#1}} @@ -307,7 +305,7 @@ % % Define an outlined section as follows: % -% \SectionDef[defines the relevant concepts;]{StableLabel}{Displayed Title} +% \SectionDef[defines the relevant concepts]{StableLabel}{Displayed Title} % % The optional first argument is the text printed after the section reference % in the outline. It should include its final punctuation. The second @@ -323,7 +321,7 @@ % Most subsections should continue to use \subsection and do not appear in the % chapter outline. To include a selected subsection, use: % -% \OutlineSubsectionDef[defines a special case;]{StableLabel}{Displayed Title} +% \OutlineSubsectionDef[defines a special case]{StableLabel}{Displayed Title} % % It is nested under the most recent \SectionDef in the same chapter, so it must % follow its intended parent section. @@ -339,7 +337,7 @@ \def\ASLChapterOutlineDescription{#3}% \ifx\ASLChapterOutlineDescription\@empty \else - \space #3% + \space #3;% \fi \@ifundefined{ASLChapterOutlineSubsections@#1@#2}{}{% \begin{itemize}% @@ -371,7 +369,7 @@ \def\ASLChapterOutlineDescription{#4}% \ifx\ASLChapterOutlineDescription\@empty \else - \space #4% + \space #4;% \fi }% }{}% diff --git a/asllib/doc/AbstractSyntax.tex b/asllib/doc/AbstractSyntax.tex index 6f518ebf4a..384c8443f4 100644 --- a/asllib/doc/AbstractSyntax.tex +++ b/asllib/doc/AbstractSyntax.tex @@ -28,7 +28,7 @@ \chapter{Abstract Syntax\label{chap:AbstractSyntax}} \ChapterOutline -\SectionDef[defines the type of Abstract Syntax Trees (ASTs) used by ASL;] +\SectionDef[defines the type of Abstract Syntax Trees (ASTs) used by ASL] {AbstractSyntaxTrees}{Abstract Syntax Trees} In an ASL abstract syntax tree, a node is one of the following data types: @@ -49,7 +49,7 @@ \chapter{Abstract Syntax\label{chap:AbstractSyntax}} The function $\substrecordfield(r, f, n)$ takes a record AST node $r$, a field name $f$ and an AST node $n$ and returns an AST record node $r'$ where the $f$ field is bound to $n$. -\SectionDef[defines notations used to define the ASTs of ASL;] +\SectionDef[defines notations used to define the ASTs of ASL] {AbstractSyntaxGrammar}{Abstract Syntax Grammar} An abstract syntax is defined in terms of derivation rules containing variables (also referred to as non-terminals). @@ -70,24 +70,24 @@ \chapter{Abstract Syntax\label{chap:AbstractSyntax}} An abstract syntax consists of a set of derivation rules and a start non-terminal. -\SectionDef[defines the AST nodes for the \untypedast:] +\SectionDef[defines the AST nodes for the \untypedast] {UntypedAbstractGrammar}{Untyped Abstract Grammar} The abstract syntax of ASL is given in terms of the derivation rules below and the start non-terminal $\spec$. % Some extra details are given by using the notation $\overtext{\textit{symbol}}{\text{detail}}$. -\OutlineSubsectionDef[defines the AST for identifiers;]{Identifiers}{Identifiers} +\OutlineSubsectionDef[defines the AST for identifiers]{Identifiers}{Identifiers} Identifiers in the AST, denoted $\Identifier$ are simply strings representing ASL identifiers. Those are obtained directly from the values of identifier tokens, $\Tidentifier(s)$. -\OutlineSubsectionDef[defines the AST for literal values;]{ASTLiterals}{Literal Values} +\OutlineSubsectionDef[defines the AST for literal values]{ASTLiterals}{Literal Values} The following rules correspond to literal values of the following ASL data types: integers, Booleans, real numbers, bitvectors, and strings. \RenderType{literal} -\OutlineSubsectionDef[defines the AST for operators;]{Operators}{Operators} +\OutlineSubsectionDef[defines the AST for operators]{Operators}{Operators} The following rules correspond to unary operators and binary operators, which can be used in unary expressions and binary expressions. @@ -143,7 +143,7 @@ \chapter{Abstract Syntax\label{chap:AbstractSyntax}} \end{tabular} \end{center} -\OutlineSubsectionDef[defines the AST for expressions;]{Expressions}{Expressions} +\OutlineSubsectionDef[defines the AST for expressions]{Expressions}{Expressions} The following rules correspond to various types of expressions: literal expressions, variable expressions, type assertions, binary operation expressions, unary operation expressions, call expressions, slicing expressions, conditional expressions, array access expressions, single-field access expressions, multiple-field access expressions, @@ -152,29 +152,29 @@ \chapter{Abstract Syntax\label{chap:AbstractSyntax}} \RenderTypes{untyped_expr} -\OutlineSubsectionDef[defines the AST for patterns;]{Patterns}{Patterns} +\OutlineSubsectionDef[defines the AST for patterns]{Patterns}{Patterns} \hypertarget{constant-zerobit}{} \hypertarget{constant-onebit}{} \hypertarget{constant-xbit}{} \RenderType{pattern} -\OutlineSubsectionDef[defines the AST for slices;]{Slices}{Slices} +\OutlineSubsectionDef[defines the AST for slices]{Slices}{Slices} \RenderTypes{untyped_slice} -\OutlineSubsectionDef[defines the AST for subprogram calls;]{SubprogramCalls}{Subprogram calls} +\OutlineSubsectionDef[defines the AST for subprogram calls]{SubprogramCalls}{Subprogram calls} \RenderType{call} -\OutlineSubsectionDef[defines the AST for types;]{Types}{Types} +\OutlineSubsectionDef[defines the AST for types]{Types}{Types} \RenderType{ty} -\OutlineSubsectionDef[defines the AST for constraints;]{Constraints}{Constraints} +\OutlineSubsectionDef[defines the AST for constraints]{Constraints}{Constraints} \RenderTypes{untyped_constraint_kind} \RenderType{int_constraint} -\OutlineSubsectionDef[defines the AST for bitfields;]{BitFields}{Bit Fields} +\OutlineSubsectionDef[defines the AST for bitfields]{BitFields}{Bit Fields} \RenderType{bitfield} -\OutlineSubsectionDef[defines the AST for fields and typed identifiers;] +\OutlineSubsectionDef[defines the AST for fields and typed identifiers] {FieldsAndTypedIdentifiers}{Fields and Typed Identifiers} The following rule corresponds to a field of a record-like structure: @@ -183,12 +183,12 @@ \chapter{Abstract Syntax\label{chap:AbstractSyntax}} The following rule corresponds to an identifier with its associated type: \RenderType{typed_identifier} -\OutlineSubsectionDef[defines the AST for assignable expressions;] +\OutlineSubsectionDef[defines the AST for assignable expressions] {AssignableExpressions}{Assignable Expressions} The following rules define the types of left-hand side of assignments: \RenderTypes{untyped_lexpr} -\OutlineSubsectionDef[defines the AST for local declarations;] +\OutlineSubsectionDef[defines the AST for local declarations] {LocalDeclarations}{Local Declarations} A local declaration keyword specifies whether a local storage declaration is mutable or immutable: \RenderType{local_decl_keyword} @@ -205,35 +205,35 @@ \chapter{Abstract Syntax\label{chap:AbstractSyntax}} \RenderType{local_decl_item} -\OutlineSubsectionDef[defines the AST for statements;]{Statements}{Statements} +\OutlineSubsectionDef[defines the AST for statements]{Statements}{Statements} \RenderTypes{untyped_stmt} \RenderType{for_direction} -\OutlineSubsectionDef[defines the AST for case alternatives;] +\OutlineSubsectionDef[defines the AST for case alternatives] {CaseAlternatives}{Case Alternatives} \RenderType{case_alt} -\OutlineSubsectionDef[defines the AST for exception catchers;] +\OutlineSubsectionDef[defines the AST for exception catchers] {ExceptionCatchers}{Exception Catchers} \RenderType{catcher} -\OutlineSubsectionDef[defines the AST for subprograms;]{Subprograms}{Subprograms} +\OutlineSubsectionDef[defines the AST for subprograms]{Subprograms}{Subprograms} \RenderType{subprogram_type} \RenderType{func_qualifier} \RenderType{override_info} \RenderType{func} -\OutlineSubsectionDef[defines the AST for global declarations;] +\OutlineSubsectionDef[defines the AST for global declarations] {GlobalDeclarations}{Global Declarations} Declaration keyword for global storage elements: \RenderType{global_decl_keyword} \RenderType{global_decl} \RenderType{decl} -\OutlineSubsectionDef[defines the AST for specifications;]{Specifications}{Specifications} +\OutlineSubsectionDef[defines the AST for specifications]{Specifications}{Specifications} \RenderType{spec} -\SectionDef[defines the \typedast;]{TypedAbstractSyntax}{Typed Abstract Syntax} +\SectionDef[defines the \typedast]{TypedAbstractSyntax}{Typed Abstract Syntax} The derivation rules for the typed abstract syntax are the same as the rules for the untyped abstract syntax, except for the following differences. @@ -288,7 +288,7 @@ \chapter{Abstract Syntax\label{chap:AbstractSyntax}} Global pragma declarations $\DPragma$ are removed from the \untypedast\ once their expressions have been typechecked and do not appear in the \typedast. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SectionDef[explains how we use inference rules to transform a parse tree into an \untypedast;] +\SectionDef[explains how we use inference rules to transform a parse tree into an \untypedast] {BuildingAbstractSyntaxTrees}{Building Abstract Syntax Trees} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% This section defines how to transform a parse tree into the corresponding AST @@ -382,7 +382,7 @@ \subsection{Abbreviated Rule Notation for AST Builders} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SectionDef[presents rules for building ASTs from parameterised productions;] +\SectionDef[presents rules for building ASTs from parameterised productions] {BuildingParameterisedProductions}{Building Parameterised Productions} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% This section defines builder relations for the @@ -550,7 +550,7 @@ \subsection{Abbreviated Rule Notation for AST Builders} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SectionDef[maps \assignableexpressions{} to right-hand side expressions;] +\SectionDef[maps \assignableexpressions{} to right-hand side expressions] {LeftToRight}{Transforming Assignable Expressions} \RenderRelation{rexpr} This function is utilised by both the type system and the dynamic semantics. diff --git a/asllib/doc/AssignableExpressions.tex b/asllib/doc/AssignableExpressions.tex index cddf5babeb..fd623518dd 100644 --- a/asllib/doc/AssignableExpressions.tex +++ b/asllib/doc/AssignableExpressions.tex @@ -42,7 +42,7 @@ \chapter{Assignable Expressions\label{chap:AssignableExpressions}} using $\texttt{eval\_expr}$ to evaluate it. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef[defines the syntax for \assignableexpressions;]{Assignable Expressions} +\SyntaxDef[defines the syntax for \assignableexpressions]{Assignable Expressions} \begin{flalign*} \Nlexpr \derives\ & \Tminus &\\ @@ -439,7 +439,7 @@ \subsection{Desugaring Assignable Expressions\label{sec:AssignableExpressionsDes \end{mathpar} \hypertarget{def-discardlexprterm}{} -\SectionDef[defines discarding assignment expressions;] +\SectionDef[defines discarding assignment expressions] {DiscardingAssignmentExpressions}{Discarding Assignment Expressions} \subsection{Abstract Syntax} \RenderTypes[remove_hypertargets]{lexpr_discard} @@ -466,7 +466,7 @@ \subsection{Semantics} \CodeSubsection{\EvalLEDiscardBegin}{\EvalLEDiscardEnd}{../Interpreter.ml} \hypertarget{def-varlexprterm}{} -\SectionDef[defines variable assignment expressions;] +\SectionDef[defines variable assignment expressions] {VariableAssignmentExpressions}{Variable Assignment Expressions} \subsection{Abstract Syntax} \RenderTypes[remove_hypertargets]{lexpr_var} @@ -507,7 +507,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_lexpr_LEVar} \CodeSubsection{\EvalLEVarBegin}{\EvalLEVarEnd}{../Interpreter.ml} -\SectionDef[defines multi-assignment expressions;] +\SectionDef[defines multi-assignment expressions] {MultiAssignmentExpressions}{Multi-assignment Expressions} \hypertarget{def-destructuringlexprterm}{} \ASLListing{Assignment to multiple left-hand-side expressions}{semantics-ledestructuring}{\semanticstests/SemanticsRule.LEDestructuring.asl} @@ -583,7 +583,7 @@ \subsection{Semantics} \RenderRule{protected_multi_assign} \hypertarget{def-setarraylexprterm}{} -\SectionDef[defines array assignment expressions;] +\SectionDef[defines array assignment expressions] {ArrayAssignmentExpressions}{Array Assignment Expressions} This section details the syntax, abstract syntax, semantics, and typing of array write expressions. @@ -623,7 +623,7 @@ \subsubsection{Comments} See \SyntacticSugarRef{SetterFieldAssignment}. \hypertarget{def-slicelexprterm}{} -\SectionDef[defines bitvector slice assignment expressions;] +\SectionDef[defines bitvector slice assignment expressions] {BitvectorSliceAssignmentExpressions}{Bitvector Slice Assignment Expressions} \ASLListing{Assignable slice expressions}{semantics-leslice}{\semanticstests/SemanticsRule.LESlice.asl} @@ -690,7 +690,7 @@ \subsubsection{Comments} \RenderProseAndFormally{check_two_ranges_non_overlapping} \hypertarget{def-setfieldlexprterm}{} -\SectionDef[defines structured type field assignment expressions;] +\SectionDef[defines structured type field assignment expressions] {StructuredTypeFieldAssignmentExpressions}{Structured Type Field Assignment Expressions} \subsection{Abstract Syntax} \RenderTypes[remove_hypertargets]{lexpr_setfield} @@ -748,7 +748,7 @@ \subsubsection{Comments} See \SyntacticSugarRef{SetterFieldAssignment}. -\SectionDef[defines structured type multi-field assignment expressions;] +\SectionDef[defines structured type multi-field assignment expressions] {StructuredTypeMultiFieldAssignmentExpressions}{Structured Type Multi-field Assignment Expressions} \ASLListing{Multi-field assignment expression}{lesetfields}{\typingtests/TypingRule.LESetFields.asl} diff --git a/asllib/doc/Bitfields.tex b/asllib/doc/Bitfields.tex index 713b8d8f83..34af28a6dd 100644 --- a/asllib/doc/Bitfields.tex +++ b/asllib/doc/Bitfields.tex @@ -27,7 +27,7 @@ \chapter{Bitfields\label{chap:Bitfields}} \ChapterOutline -\SectionDef[describes nested bitfields;] +\SectionDef[describes nested bitfields] {Nested Bitfields}{Nested Bitfields} Bitfields may have nested bitfields. This can have several uses, one of which is being able to define two different views of a register. @@ -87,7 +87,7 @@ \chapter{Bitfields\label{chap:Bitfields}} \ASLListing{A bitvector type with nested bitfields}{nestedbitfields}{\definitiontests/Bitfields_nested.asl} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for bitfields;]{Bitfields} +\FormalRelationsDef[defines the formal relations for bitfields]{Bitfields} \paragraph{Syntax:} Bitfields are grammatically derived from $\Nbitfield$ and lists of bitfields are grammatically derived from $\Nbitfields$. @@ -102,7 +102,7 @@ \chapter{Bitfields\label{chap:Bitfields}} $\evallexpr$ (see \secref{BitvectorSliceAssignmentExpressions}). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef[defines the syntax of bitfields;]{Bitfields} +\SyntaxDef[defines the syntax of bitfields]{Bitfields} \begin{flalign*} \Nbitfields \derives \ & \Tlbrace \parsesep \TClistZero{\Nbitfield} \parsesep \Trbrace &\\ \Nbitfield \derives \ & \Nslices \parsesep \Tidentifier &\\ @@ -111,7 +111,7 @@ \chapter{Bitfields\label{chap:Bitfields}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef[defines the abstract syntax of bitfields;]{Bitfields} +\AbstractSyntaxDef[defines the abstract syntax of bitfields]{Bitfields} \RenderType[remove_hypertargets]{bitfield} \ASTRuleDef{Bitfields} diff --git a/asllib/doc/BlockStatements.tex b/asllib/doc/BlockStatements.tex index c82b593619..7f8209862f 100644 --- a/asllib/doc/BlockStatements.tex +++ b/asllib/doc/BlockStatements.tex @@ -24,7 +24,7 @@ \chapter{Block Statements\label{chap:BlockStatements}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for block statements;]{Block Statements} +\FormalRelationsDef[defines the formal relations for block statements]{Block Statements} \paragraph{Syntax:} Block statements are grammatically the same as other statements derived from $\Nstmt$. diff --git a/asllib/doc/CatchingExceptions.tex b/asllib/doc/CatchingExceptions.tex index 126027eddf..4db7d72bcb 100644 --- a/asllib/doc/CatchingExceptions.tex +++ b/asllib/doc/CatchingExceptions.tex @@ -24,7 +24,7 @@ \chapter{Catching Exceptions\label{chap:CatchingExceptions}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for exception catchers;]{Exception Catchers} +\FormalRelationsDef[defines the formal relations for exception catchers]{Exception Catchers} \paragraph{Syntax:} Exception catchers are grammatically derived from $\Ncatcher$. \paragraph{Abstract Syntax:} Exception catchers are derived in the abstract syntax by $\catcher$ and generated using $\buildcatcher$. @@ -32,14 +32,14 @@ \chapter{Catching Exceptions\label{chap:CatchingExceptions}} \paragraph{Semantics:} Exception catchers are evaluated via $\evalcatchers$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef[defines the syntax of exception catchers;]{Exception Catchers} +\SyntaxDef[defines the syntax of exception catchers]{Exception Catchers} \begin{flalign*} \Ncatcher \derives \ & \Twhen \parsesep \Tidentifier \parsesep \Tcolon \parsesep \Nty \parsesep \Tarrow \parsesep \Nstmtlist &\\ |\ & \Twhen \parsesep \Nty \parsesep \Tarrow \parsesep \Nstmtlist &\\ \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef[defines the abstract syntax of exception catchers;]{Exception Catchers} +\AbstractSyntaxDef[defines the abstract syntax of exception catchers]{Exception Catchers} \RenderType[remove_hypertargets]{catcher} \ASTRuleDef{Catcher} @@ -77,7 +77,7 @@ \chapter{Catching Exceptions\label{chap:CatchingExceptions}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef[defines the type rules for exception catchers;]{Exception Catchers} +\TypeRulesDef[defines the type rules for exception catchers]{Exception Catchers} \RenderRelation{annotate_catcher} \TypingRuleDef{Catcher} diff --git a/asllib/doc/ErrorCodes.tex b/asllib/doc/ErrorCodes.tex index ba30750b1a..78b89ab95f 100644 --- a/asllib/doc/ErrorCodes.tex +++ b/asllib/doc/ErrorCodes.tex @@ -96,7 +96,7 @@ \chapter{Errors\label{chap:Errors}} \end{Verbatim} % CONSOLE_END -\SectionDef[defines a classification of ASL errors;] +\SectionDef[defines a classification of ASL errors] {Error Kinds}{Error Kinds} \hypertarget{def-errorcodeterm}{} Each type of error has an \emph{\errorcodeterm}, which uniquely identifies it @@ -130,7 +130,7 @@ \chapter{Errors\label{chap:Errors}} \Builderrorsterm{} and \typingerrorsterm{} are known collectively as \staticerrorsterm. -\SectionDef[summarises the error codes used throughout this reference;] +\SectionDef[summarises the error codes used throughout this reference] {ErrorCodesSummary}{Error Codes Summary} The following table summarises all error codes. @@ -179,7 +179,7 @@ \chapter{Errors\label{chap:Errors}} \end{tabular} \end{center} -\SectionDef[details \builderrorsterm;] +\SectionDef[details \builderrorsterm] {BuildErrors}{Build Errors} \begin{description} \item[$\LexicalError$] @@ -211,7 +211,7 @@ \chapter{Errors\label{chap:Errors}} For example, the standard library defines a non-subprogram (\ASTRuleRef{SetBuiltin}). \end{description} -\SectionDef[details \typingerrorsterm;] +\SectionDef[details \typingerrorsterm] {TypingErrors}{Type Errors} \begin{description} diff --git a/asllib/doc/Expressions.tex b/asllib/doc/Expressions.tex index c268330af4..45297adebe 100644 --- a/asllib/doc/Expressions.tex +++ b/asllib/doc/Expressions.tex @@ -19,7 +19,7 @@ \chapter{Expressions\label{chap:Expressions}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for expressions;]{Expressions} +\FormalRelationsDef[defines the formal relations for expressions]{Expressions} \paragraph{Syntax:} Expressions are grammatically derived from $\Nexpr$. \paragraph{Abstract Syntax:} Expressions are derived in the abstract syntax from $\expr$, @@ -45,7 +45,7 @@ \chapter{Expressions\label{chap:Expressions}} \paragraph{Semantics:} \RenderRelation{eval_expr} \hypertarget{def-literalexpressionterm}{} -\SectionDef[defines \literalexpressionsterm;] +\SectionDef[defines \literalexpressionsterm] {LiteralExpressions}{Literal Expressions} A literal expression represents a literal as an expression. @@ -86,7 +86,7 @@ \subsection{Semantics} \CodeSubsection{\EvalELitBegin}{\EvalELitEnd}{../Interpreter.ml} \hypertarget{def-variableexpressionterm}{} -\SectionDef[defines \variableexpressionsterm;] +\SectionDef[defines \variableexpressionsterm] {VariableExpressions}{Variable Expressions} A variable expression consists of an identifier for a storage element. @@ -142,7 +142,7 @@ \subsubsection{Comments} \TypingRuleRef{DeclareGlobalStorage}, and \TypingRuleRef{DeclareOneFunc}. \hypertarget{def-binopexpressionterm}{} -\SectionDef[defines \binopexpressionsterm;] +\SectionDef[defines \binopexpressionsterm] {BinaryExpressions}{Binary Expressions} Binary expressions apply a binary operator to two sub-expressions. @@ -521,7 +521,7 @@ \subsubsection{Comments} as well as \texttt{==}). \hypertarget{def-unopexpressionterm}{} -\SectionDef[defines \unopexpressionsterm;] +\SectionDef[defines \unopexpressionsterm] {UnaryExpressions}{Unary Expressions} \subsection{Syntax} \begin{flalign*} @@ -561,7 +561,7 @@ \subsection{Semantics} \CodeSubsection{\EvalUnopBegin}{\EvalUnopEnd}{../Interpreter.ml} \hypertarget{def-conditionexpressionterm}{} -\SectionDef[defines \condexpressionsterm;] +\SectionDef[defines \condexpressionsterm] {ConditionalExpressions}{Conditional Expressions} \subsection{Syntax} \begin{flalign*} @@ -628,7 +628,7 @@ \subsection{Semantics} \CodeSubsection{\EvalECondBegin}{\EvalECondEnd}{../Interpreter.ml} \hypertarget{def-callexpressionterm}{} -\SectionDef[defines \callexpressionsterm;] +\SectionDef[defines \callexpressionsterm] {CallExpressions}{Call Expressions} \ASLListing{Call expressions}{semantics-ecall}{\semanticstests/SemanticsRule.ECall.asl} @@ -736,7 +736,7 @@ \subsection{Semantics} \CodeSubsection{\EvalECallBegin}{\EvalECallEnd}{../Interpreter.ml} \hypertarget{def-slicingexpressionsterm}{} -\SectionDef[defines \slicingexpressionsterm;] +\SectionDef[defines \slicingexpressionsterm] {SlicingExpressions}{Slicing Expressions} This section details the high-level form of the syntax and abstract syntax of slicing expressions, and defines the semantics of bitvector slices. @@ -810,7 +810,7 @@ \subsection{Semantics} \hypertarget{def-arrayaccessexpressionsterm}{} \hypertarget{def-getarrayexpressionterm}{} -\SectionDef[defines \arrayaccessexpressionsterm;] +\SectionDef[defines \arrayaccessexpressionsterm] {ArrayAccessExpressions}{Array Access Expressions} This section details the syntax, abstract syntax, semantics, and typing of array read expressions. @@ -876,7 +876,7 @@ \subsection{Abstract Syntax} \CodeSubsection{\EvalEGetArrayBegin}{\EvalEGetArrayEnd}{../Interpreter.ml} \hypertarget{def-getfieldexpressionterm}{} -\SectionDef[defines field reading expressions;] +\SectionDef[defines field reading expressions] {FieldReadingExpressions}{Field Reading Expressions} \subsection{Syntax} \begin{flalign*} @@ -987,7 +987,7 @@ \subsection{Semantics} \CodeSubsection{\EvalEGetTupleItemBegin}{\EvalEGetTupleItemEnd}{../Interpreter.ml} \hypertarget{def-getfieldsexpressionterm}{} -\SectionDef[defines multi-field reading expressions;] +\SectionDef[defines multi-field reading expressions] {MultiFieldReadingExpressions}{Multi-field Reading Expressions} \subsection{Syntax} \begin{flalign*} @@ -1088,7 +1088,7 @@ \subsection{Semantics} \CodeSubsection{\EvalEGetCollectionFieldsBegin}{\EvalEGetCollectionFieldsEnd}{../Interpreter.ml} \hypertarget{def-atceexpressionterm}{} -\SectionDef[defines asserting type conversion expressions;] +\SectionDef[defines asserting type conversion expressions] {AssertingTypeConversionExpressions}{Asserting Type Conversion Expressions} The rule about domains in the definitions of subtype-satisfaction and type-satisfaction means that it is illegal to use the unconstrained integer @@ -1261,7 +1261,7 @@ \subsubsection{Comments} \RenderProseAndFormally{is_constraint_sat} \hypertarget{def-patternexpressionterm}{} -\SectionDef[defines pattern matching expressions;] +\SectionDef[defines pattern matching expressions] {PatternMatchingExpressions}{Pattern Matching Expressions} The binary operator $\Tin$ tests whether a value (referred to as the discriminant) matches any item from a $\Npatternset$. Patterns can also be used to test whether an expression matches a bitmask. @@ -1346,7 +1346,7 @@ \subsection{Semantics} \CodeSubsection{\EvalEPatternBegin}{\EvalEPatternEnd}{../Interpreter.ml} \hypertarget{def-arbitraryexpressionterm}{} -\SectionDef[defines arbitrary value expressions;] +\SectionDef[defines arbitrary value expressions] {ArbitraryValueExpressions}{Arbitrary Value Expressions} An expression of the form \texttt{ARBITRARY: ty} evaluates to an arbitrary value in the domain of \texttt{ty}. @@ -1416,7 +1416,7 @@ \subsubsection{Comments} Notice that this rule introduces non-determinism. -\SectionDef[defines structured type construction expressions;] +\SectionDef[defines structured type construction expressions] {StructuredTypeConstructionExpressions}{Structured Type Construction Expressions} \hypertarget{def-recordexpressionterm}{} \listingref{semantics-egetfield} shows an example of a well-typed record construction expression. @@ -1511,7 +1511,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_expr_ERecord} \CodeSubsection{\EvalERecordBegin}{\EvalERecordEnd}{../Interpreter.ml} -\SectionDef[defines tuple expressions;] +\SectionDef[defines tuple expressions] {TupleExpressions}{Tuple Expressions} \hypertarget{def-tupleexpressionterm}{} @@ -1554,7 +1554,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_expr_ETuple} \CodeSubsection{\EvalETupleBegin}{\EvalETupleEnd}{../Interpreter.ml} -\SectionDef[defines parenthesised expressions;] +\SectionDef[defines parenthesised expressions] {ParenthesisedExpressions}{Parenthesised Expressions} A single expression inside parentheses is not considered to be a tuple, but rather the element inside the parenthesis. @@ -1587,7 +1587,7 @@ \subsection{Abstract Syntax} } \end{mathpar} -\SectionDef[defines array construction expressions;] +\SectionDef[defines array construction expressions] {ArrayConstructionExpressions}{Array Construction Expressions} Array construction expression are used by the type system to express the initialisation of array-typed variables. Since there is no syntax to initialise arrays, there are also @@ -1614,7 +1614,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_expr_EArray} \CodeSubsection{\EvalEArrayBegin}{\EvalEArrayEnd}{../Interpreter.ml} -\SectionDef[defines \sideeffectfreeexpressionsterm{};] +\SectionDef[defines \sideeffectfreeexpressionsterm{}] {SideEffectFreeExpressions}{Side-effect-free Expressions} \subsection{Typing} \texthypertarget{def-sideeffectfreeexpressionterm} diff --git a/asllib/doc/GlobalPragmas.tex b/asllib/doc/GlobalPragmas.tex index 68242d11f1..a7cedbb915 100644 --- a/asllib/doc/GlobalPragmas.tex +++ b/asllib/doc/GlobalPragmas.tex @@ -18,7 +18,7 @@ \chapter{Global Pragma Declarations\label{chap:Global Pragma Declarations}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for global pragma declarations;]{Global Pragma Declarations} +\FormalRelationsDef[defines the formal relations for global pragma declarations]{Global Pragma Declarations} \paragraph{Syntax:} Global pragma declarations are grammatically derived from $\Ndecl$. \paragraph{Abstract Syntax:} Global pragma declarations are derived in the abstract syntax from $\decl$, @@ -30,7 +30,7 @@ \chapter{Global Pragma Declarations\label{chap:Global Pragma Declarations}} they have no associated dynamic semantics. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef[defines the syntax of global pragma declarations;]{Global Pragma Declarations} +\SyntaxDef[defines the syntax of global pragma declarations]{Global Pragma Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{flalign*} diff --git a/asllib/doc/GlobalStorageDeclarations.tex b/asllib/doc/GlobalStorageDeclarations.tex index 4f941107d7..a037c83542 100644 --- a/asllib/doc/GlobalStorageDeclarations.tex +++ b/asllib/doc/GlobalStorageDeclarations.tex @@ -47,7 +47,7 @@ \chapter{Global Storage Declarations\label{chap:GlobalStorageDeclarations}} The semantics of a single global storage declaration is defined in \SemanticsRuleRef{DeclareGlobal}. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef[defines the syntax of global storage declarations;]{Global Storage Declarations} +\SyntaxDef[defines the syntax of global storage declarations]{Global Storage Declarations} \RequirementDef{DiscardingGlobalStorageDeclarations} Global storage declarations must\\ bind a name. This is ensured by the ASL grammar. @@ -70,7 +70,7 @@ \chapter{Global Storage Declarations\label{chap:GlobalStorageDeclarations}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef[defines the abstract syntax of global storage declarations;]{Global Storage Declarations} +\AbstractSyntaxDef[defines the abstract syntax of global storage declarations]{Global Storage Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RenderTypes[remove_hypertargets]{decl_global_storage} @@ -242,7 +242,7 @@ \chapter{Global Storage Declarations\label{chap:GlobalStorageDeclarations}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef[defines the type rules of global storage declarations;]{Global Storage Declarations} +\TypeRulesDef[defines the type rules of global storage declarations]{Global Storage Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RequirementDef{GlobalStorageCycles} diff --git a/asllib/doc/Literals.tex b/asllib/doc/Literals.tex index 929f6dfe18..de03e45c7b 100644 --- a/asllib/doc/Literals.tex +++ b/asllib/doc/Literals.tex @@ -18,7 +18,7 @@ \chapter{Literals\label{chap:Literals}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for literals;]{Literals} +\FormalRelationsDef[defines the formal relations for literals]{Literals} \paragraph{Syntax:} Literals are grammatically derived from $\Nvalue$. \paragraph{Abstract Syntax:} Literals are derived in abstract syntax from $\literal$. The function $\buildvalue$ transforms a parse node for $\Nvalue$, except for enumeration labels, @@ -28,7 +28,7 @@ \chapter{Literals\label{chap:Literals}} (see \SemanticsRulesRef{Literals}). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef[defines the syntax for literals;]{Literals} +\SyntaxDef[defines the syntax for literals]{Literals} \begin{flalign*} \Nvalue \derives \ & \Tintlit &\\ |\ & \Tboollit &\\ @@ -38,7 +38,7 @@ \chapter{Literals\label{chap:Literals}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef[defines the abstract syntax and the abstract syntax builders for literals;]{Literals} +\AbstractSyntaxDef[defines the abstract syntax and the abstract syntax builders for literals]{Literals} \RenderType[remove_hypertargets]{literal} \subsection{ASTRule.Value \label{sec:ASTRule.Value}} diff --git a/asllib/doc/LocalStorageDeclarations.tex b/asllib/doc/LocalStorageDeclarations.tex index 6982cac466..ee1dc94f0f 100644 --- a/asllib/doc/LocalStorageDeclarations.tex +++ b/asllib/doc/LocalStorageDeclarations.tex @@ -11,7 +11,7 @@ \chapter{Local Storage Declarations\label{chap:LocalStorageDeclarations}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for local storage declarations;]{Local Storage Declarations} +\FormalRelationsDef[defines the formal relations for local storage declarations]{Local Storage Declarations} \paragraph{Syntax:} Local storage declarations are grammatically derived from statements ($\Nstmt$) via dedicated rules (see \SyntaxRef{Local Storage Declarations}). @@ -31,7 +31,7 @@ \chapter{Local Storage Declarations\label{chap:LocalStorageDeclarations}} This is used to evaluate both single local storage declarations and tuples of local storage declarations. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef[defines the syntax of local storage declarations;]{Local Storage Declarations} +\SyntaxDef[defines the syntax of local storage declarations]{Local Storage Declarations} \hypertarget{def-localdeclarationkeyword}{} \hypertarget{def-localdeclarationitem}{} A \localdeclarationkeyword\ is either \texttt{var} or \texttt{let}. @@ -55,7 +55,7 @@ \chapter{Local Storage Declarations\label{chap:LocalStorageDeclarations}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef[defines the abstract syntax of local storage declarations;]{Local Storage Declarations} +\AbstractSyntaxDef[defines the abstract syntax of local storage declarations]{Local Storage Declarations} \RenderTypes[remove_hypertargets]{local_decl_keyword_and_item} @@ -151,7 +151,7 @@ \chapter{Local Storage Declarations\label{chap:LocalStorageDeclarations}} } \end{mathpar} -\SectionDef[defines the type rules of local variable declarations;] +\SectionDef[defines the type rules of local variable declarations] {Typing of Local Variable Declarations}{Typing of Local Variable Declarations} \TypingRuleDef{LDVar} \ExampleDef{Well-typed Local Variable Declarations} @@ -200,7 +200,7 @@ \chapter{Local Storage Declarations\label{chap:LocalStorageDeclarations}} \CodeSubsection{\CheckIsNotCollectionBegin}{\CheckIsNotCollectionEnd}{../Typing.ml} -\SectionDef[defines the dynamic semantics of local variable declarations;] +\SectionDef[defines the dynamic semantics of local variable declarations] {Semantics of Local Variable Declarations}{Semantics of Local Variable Declarations} \SemanticsRuleDef{LDVar} \ExampleDef{Evaluation of a Local Variable Declaration} @@ -211,7 +211,7 @@ \chapter{Local Storage Declarations\label{chap:LocalStorageDeclarations}} \RenderProseAndFormally{eval_local_decl_LDI_Var} \CodeSubsection{\EvalLDVarBegin}{\EvalLDVarEnd}{../Interpreter.ml} -\SectionDef[defines the type rules of tuples of local storage declarations;] +\SectionDef[defines the type rules of tuples of local storage declarations] {Typing of Tuple Declarations}{Typing of Tuple Declarations} \TypingRuleDef{LDTuple} \ExampleDef{Well-typed Tuple Declarations} diff --git a/asllib/doc/PatternMatching.tex b/asllib/doc/PatternMatching.tex index 0b4441b9cb..6a847e00cb 100644 --- a/asllib/doc/PatternMatching.tex +++ b/asllib/doc/PatternMatching.tex @@ -11,7 +11,7 @@ \chapter{Pattern Matching\label{chap:PatternMatching}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for patterns;]{Patterns} +\FormalRelationsDef[defines the formal relations for patterns]{Patterns} \paragraph{Syntax:} Patterns are grammatically derived from $\Npattern$. \paragraph{Abstract Syntax:} Patterns are derived in the abstract grammar from $\pattern$ @@ -29,7 +29,7 @@ \chapter{Pattern Matching\label{chap:PatternMatching}} \paragraph{Semantics:} Patterns are evaluated by $\evalpattern$. \RenderRelation{eval_pattern} -\SectionDef[defines the match-all-values pattern;] +\SectionDef[defines the match-all-values pattern] {MatchingAllValues}{Matching All Values} \hypertarget{any-pattern}{} \ASLListing{Matching any value}{semantics-pall}{\semanticstests/SemanticsRule.PAll.asl} @@ -67,7 +67,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_pattern_PAll} \CodeSubsection{\EvalPAllBegin}{\EvalPAllEnd}{../Interpreter.ml} -\SectionDef[defines the match-a-single-value pattern;] +\SectionDef[defines the match-a-single-value pattern] {MatchingASingleValue}{Matching a Single Value} \subsection{Syntax} \begin{flalign*} @@ -109,7 +109,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_pattern_PSingle} \CodeSubsection{\EvalPSingleBegin}{\EvalPSingleEnd}{../Interpreter.ml} -\SectionDef[defines the match-a-range-of-integers pattern;] +\SectionDef[defines the match-a-range-of-integers pattern] {MatchingARangeOfIntegers}{Matching a Range of Integers} \subsection{Syntax} \begin{flalign*} @@ -158,7 +158,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_pattern_PRange} \CodeSubsection{\EvalPRangeBegin}{\EvalPRangeEnd}{../Interpreter.ml} -\SectionDef[defines the less-than-or-equal pattern;] +\SectionDef[defines the less-than-or-equal pattern] {MatchingAnUpperBoundedRangeOfIntegers}{Matching an Upper Bounded Range of Integers} \subsection{Syntax} \begin{flalign*} @@ -201,7 +201,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_pattern_PLeq} \CodeSubsection{\EvalPLeqBegin}{\EvalPLeqEnd}{../Interpreter.ml} -\SectionDef[defines the greater-than-or-equal pattern;] +\SectionDef[defines the greater-than-or-equal pattern] {MatchingALowerBoundedRangeOfIntegers}{Matching a Lower Bounded Range of Integers} \subsection{Syntax} \begin{flalign*} @@ -244,7 +244,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_pattern_PGeq} \CodeSubsection{\EvalPGeqBegin}{\EvalPGeqEnd}{../Interpreter.ml} -\SectionDef[defines the bitmask pattern;] +\SectionDef[defines the bitmask pattern] {MatchingABitmask}{Matching a Bitmask} Bitmasks are used to match sets of bitvectors where occurrences of $\xbit$, and bit sequences in parentheses represent, don't-care values. diff --git a/asllib/doc/PrimitiveOperations.tex b/asllib/doc/PrimitiveOperations.tex index 9d2ae8066c..285ae68605 100644 --- a/asllib/doc/PrimitiveOperations.tex +++ b/asllib/doc/PrimitiveOperations.tex @@ -21,7 +21,7 @@ \chapter{Primitive Operations\label{chap:PrimitiveOperations}} \ChapterOutline -\FormalRelationsDef[defines the formal relations for primitive operations;]{Primitive Operations} +\FormalRelationsDef[defines the formal relations for primitive operations]{Primitive Operations} \paragraph{Syntax:} primitive operations are grammatically derived from $\Nunop$ and $\Nbinop$. \paragraph{Abstract Syntax:} primitive operations are derived in the abstract syntax from $\unop$ @@ -41,7 +41,7 @@ \chapter{Primitive Operations\label{chap:PrimitiveOperations}} and binary operations are dynamically evaluated via $\evalbinop$ (see \SemanticsRuleRef{BinopValues}). -\SyntaxDef[defines the syntax for unary operations and binary operations;]{Primitive Operations} +\SyntaxDef[defines the syntax for unary operations and binary operations]{Primitive Operations} \begin{flalign*} \Nunop \derivesinline\ & \Tbnot \;|\; \Tminus \;|\; \Tnot &\\ \Nbinop \derivesinline\ & \Tand \;|\; \Tband \;|\; \Tbor \;|\; \Tbeq \;|\; \Tdiv \;|\; \Tdivrm \;|\; \Txor \;|\; \Teqop \;|\; \Tneq &\\ @@ -49,7 +49,7 @@ \chapter{Primitive Operations\label{chap:PrimitiveOperations}} |\ & \Tor \;|\; \Trdiv \;|\; \Tshl \;|\; \Tshr \;|\; \Tpow \;|\; \Tcoloncolon \;|\; \Tplusplus \end{flalign*} -\AbstractSyntaxDef[defines the AST for unary operations and binary operations;]{Primitive Operations} +\AbstractSyntaxDef[defines the AST for unary operations and binary operations]{Primitive Operations} \RenderTypes[remove_hypertargets]{unop_and_binop} @@ -243,7 +243,7 @@ \chapter{Primitive Operations\label{chap:PrimitiveOperations}} } \end{mathpar} -\SectionDef[defines the signatures for all primitive operations;] +\SectionDef[defines the signatures for all primitive operations] {PrimitiveOperationSignatures}{Primitive Operation Signatures} ASL follows the mathematical and programming language tradition of allowing operators such as \texttt{+} to be overloaded to refer to one of several different operations. @@ -490,7 +490,7 @@ \chapter{Primitive Operations\label{chap:PrimitiveOperations}} \end{table} \clearpage -\SectionDef[defines the valid sets of operand values for primitive operations;] +\SectionDef[defines the valid sets of operand values for primitive operations] {PrimitiveOperationDomains}{Primitive Operation Domains} The unary operations ($\aslnotbool$, $\negateint$, $\negatereal$, and $\notbits$) are valid for all possible literal values, and most binary operations are also valid for all possible combinations of literal values of their operands. @@ -529,7 +529,7 @@ \chapter{Primitive Operations\label{chap:PrimitiveOperations}} \end{tabular} \end{center} -\TypeRulesDef[defines the static evaluation of primitive operations for literal values;]{Primitive Operations} +\TypeRulesDef[defines the static evaluation of primitive operations for literal values]{Primitive Operations} \TypingRuleDef{UnopLiterals} \RenderRelation{unop_literals} diff --git a/asllib/doc/Semantics.tex b/asllib/doc/Semantics.tex index 689d8b7ca6..b0fee886d5 100644 --- a/asllib/doc/Semantics.tex +++ b/asllib/doc/Semantics.tex @@ -84,7 +84,7 @@ \chapter{Dynamic Semantics Definitions\label{chap:Semantics}} Technically, the sequential semantics are defined by omitting the concurrent execution graph components from all \semanticsconfigurationsterm{}. -\SectionDef[defines the configurations used by the dynamic semantics;] +\SectionDef[defines the configurations used by the dynamic semantics] {Dynamic Semantics Configurations}{Dynamic Semantics Configurations} This section defines the mathematical types over which our dynamic semantics are defined. An \hyperlink{eval-example}{example} of semantic evaluation appears at the end. @@ -114,7 +114,7 @@ \chapter{Dynamic Semantics Definitions\label{chap:Semantics}} \hypertarget{def-nativevalue}{} \hypertarget{def-nativevalues}{} -\SectionDef[defines the concept of \nativevaluesterm{};] +\SectionDef[defines the concept of \nativevaluesterm{}] {nativevalues}{Native Values} Semantic evaluation binds values to storage elements when a specification is semantically evaluated. To formalise this, we define the set of \emph{\nativevaluesterm} as follows diff --git a/asllib/doc/SideEffects.tex b/asllib/doc/SideEffects.tex index 5fbd588d0e..88ebd0d894 100644 --- a/asllib/doc/SideEffects.tex +++ b/asllib/doc/SideEffects.tex @@ -13,7 +13,7 @@ \chapter{Side Effects\label{chap:SideEffects}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SectionDef[defines the concept of expression \purities{};] +\SectionDef[defines the concept of expression \purities{}] {Purity}{Purity} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/asllib/doc/Slicing.tex b/asllib/doc/Slicing.tex index 942d4d81c9..3fa107b721 100644 --- a/asllib/doc/Slicing.tex +++ b/asllib/doc/Slicing.tex @@ -13,7 +13,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for bitvector slices;]{Bitvector Slices} +\FormalRelationsDef[defines the formal relations for bitvector slices]{Bitvector Slices} \paragraph{Syntax:} Bitvector slices are grammatically derived from $\Nslice$. \paragraph{Abstract Syntax:} Bitvector slices are derived in the abstract syntax from $\slice$, @@ -24,7 +24,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \paragraph{Semantics:} Bitvector slices are evaluated by $\evalslice$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef[defines the syntax of bitvector slices;]{Bitvector Slices} +\SyntaxDef[defines the syntax of bitvector slices]{Bitvector Slices} \begin{flalign*} \Nslice \derives \ & \Nexpr &\\ |\ & \Nexpr \parsesep \Tcolon \parsesep \Nexpr &\\ @@ -32,7 +32,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef[defines the abstract syntax of bitvector slices;]{Bitvector Slices} +\AbstractSyntaxDef[defines the abstract syntax of bitvector slices]{Bitvector Slices} \RenderTypes[remove_hypertargets]{untyped_slice} \ASTRuleDef{Slice} @@ -74,7 +74,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef[defines the type rules for bitvector slices;]{Bitvector Slices} +\TypeRulesDef[defines the type rules for bitvector slices]{Bitvector Slices} \TypingRuleDef{Slice} \RenderRelation{annotate_slice} @@ -129,7 +129,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \CodeSubsection{\SymbolicConstrainedIntegerBegin}{\SymbolicConstrainedIntegerEnd}{../Typing.ml} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SemanticsRulesDef[defines the dynamic semantics of bitvector slices;]{Bitvector Slices} +\SemanticsRulesDef[defines the dynamic semantics of bitvector slices]{Bitvector Slices} \SemanticsRuleDef{Slice} \RenderRelation{eval_slice} @@ -150,7 +150,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \RenderProseAndFormally{eval_slice} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for lists of bitvector slices;]{Lists of Bitvector Slices} +\FormalRelationsDef[defines the formal relations for lists of bitvector slices]{Lists of Bitvector Slices} \paragraph{Syntax:} Lists of bitvector slices are grammatically derived from $\Nslices$. \paragraph{Abstract Syntax:} Lists of bitvector slices are represented by a list of $\slice$ @@ -161,13 +161,13 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \paragraph{Semantics:} Lists of bitvector slices are evaluated by $\evalslices$\\ (see \SemanticsRuleRef{Slices}). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef[defines the syntax of lists of bitvector slices;]{Lists of Bitvector Slices} +\SyntaxDef[defines the syntax of lists of bitvector slices]{Lists of Bitvector Slices} \begin{flalign*} \Nslices \derives \ & \Tlbracket \parsesep \ClistOne{\Nslice} \parsesep \Trbracket & \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef[defines the abstract syntax of lists of bitvector slices;]{Lists of Bitvector Slices} +\AbstractSyntaxDef[defines the abstract syntax of lists of bitvector slices]{Lists of Bitvector Slices} \ASTRuleDef{Slices} \NotImportedToASLSpecYet{ \hypertarget{build-slices}{} @@ -189,7 +189,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\TypeRulesDef[defines the type rules for lists of bitvector slices;]{Lists of Bitvector Slices} +\TypeRulesDef[defines the type rules for lists of bitvector slices]{Lists of Bitvector Slices} \TypingRuleDef{Slices} \RenderRelation{annotate_slices} @@ -203,7 +203,7 @@ \chapter{Bitvector Slices\label{chap:BitvectorSlicing}} \RenderProseAndFormally{annotate_slices} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SemanticsRulesDef[defines the dynamic semantics rules for lists of bitvector slices;]{Lists of Bitvector Slices} +\SemanticsRulesDef[defines the dynamic semantics rules for lists of bitvector slices]{Lists of Bitvector Slices} \SemanticsRuleDef{Slices} \RenderRelation{eval_slices} diff --git a/asllib/doc/Specifications.tex b/asllib/doc/Specifications.tex index 9749d44ef7..eb6dd33fa6 100644 --- a/asllib/doc/Specifications.tex +++ b/asllib/doc/Specifications.tex @@ -18,7 +18,7 @@ \chapter{Specifications\label{chap:Specifications}} \ChapterOutline -\SectionDef[defines the formal relations used for specifications;] +\SectionDef[defines the formal relations used for specifications] {Formal Relations for Specifications}{Formal Relations for Specifications} \hypertarget{def-specificationterm}{} @@ -72,7 +72,7 @@ \chapter{Specifications\label{chap:Specifications}} $\evalglobals$ and subprogram declarations are evaluated via $\evalcall$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SectionDef[defines the syntax of specifications;] +\SectionDef[defines the syntax of specifications] {Syntax of Specifications}{Syntax of Specifications} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{flalign*} @@ -80,7 +80,7 @@ \chapter{Specifications\label{chap:Specifications}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SectionDef[defines the abstract syntax of specifications;] +\SectionDef[defines the abstract syntax of specifications] {Abstract Syntax of Specifications}{Abstract Syntax of Specifications} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RenderType[remove_hypertargets]{spec} @@ -108,7 +108,7 @@ \chapter{Specifications\label{chap:Specifications}} \end{mathpar} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SectionDef[defines the type rules for specifications;] +\SectionDef[defines the type rules for specifications] {Typing Specifications}{Typing Specifications} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -304,7 +304,7 @@ \chapter{Specifications\label{chap:Specifications}} \RenderProseAndFormally{add_subprogram_decls} -\SectionDef[defines subprogram overriding and the associated type rules;] +\SectionDef[defines subprogram overriding and the associated type rules] {Overriding Subprograms}{Overriding Subprograms} This section defines how to override subprograms in a specification. In particular, a subprogram marked by \texttt{impdef} can be overridden by a subprogram marked by \\ @@ -396,7 +396,7 @@ \chapter{Specifications\label{chap:Specifications}} \RenderProseAndFormally{rename_subprograms} -\SectionDef[defines defined-used relations used to sort global declarations;] +\SectionDef[defines defined-used relations used to sort global declarations] {TopologicalOrdering}{Defined-Used Dependencies for Global Declarations} This section defines how to construct a graph of \defusedependenciesterm\ between the identifiers associated with global declarations. @@ -589,7 +589,7 @@ \chapter{Specifications\label{chap:Specifications}} \RenderProseAndFormally{use_catcher} -\SectionDef[defines how the global declarations in a specification are sorted;] +\SectionDef[defines how the global declarations in a specification are sorted] {Dependencies}{Ordering Global Declarations via Defined-Used Dependencies} \begin{definition}[Strongly Connected Components] \hypertarget{relation-scc}{} diff --git a/asllib/doc/Statements.tex b/asllib/doc/Statements.tex index 7d93150eaa..613da0cdbb 100644 --- a/asllib/doc/Statements.tex +++ b/asllib/doc/Statements.tex @@ -8,7 +8,7 @@ \chapter{Statements\label{chap:Statements}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations used for statements;]{Statements} +\FormalRelationsDef[defines the formal relations used for statements]{Statements} \paragraph{Syntax:} Statements are grammatically derived from $\Nstmt$. \paragraph{Abstract Syntax:} Statements are derived in the abstract syntax from $\stmt$ @@ -30,7 +30,7 @@ \chapter{Statements\label{chap:Statements}} \RenderRelation{eval_stmt} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SectionDef[defines pass statements;] +\SectionDef[defines pass statements] {PassStatements}{Pass Statements} \hypertarget{def-passstatementterm}{} @@ -74,7 +74,7 @@ \subsection{Semantics} \CodeSubsection{\EvalSPassBegin}{\EvalSPassEnd}{../Interpreter.ml} \hypertarget{def-assignmentstatementterm}{} -\SectionDef[defines assignment statements;] +\SectionDef[defines assignment statements] {AssignmentStatements}{Assignment Statements} \subsection{Syntax} \begin{flalign*} @@ -160,7 +160,7 @@ \subsection{Semantics} \RenderProseAndFormally{lexpr_is_var} -\SectionDef[defines setter assignment statements;] +\SectionDef[defines setter assignment statements] {SetterAssignmentStatements}{Setter Assignment Statements} \subsection{Syntax} \begin{flalign*} @@ -377,7 +377,7 @@ \subsection{Typing and semantics} As given by applying the relevant rules to the desugared AST. \hypertarget{def-declarationstatementterm}{} -\SectionDef[defines declaration statements;] +\SectionDef[defines declaration statements] {DeclarationStatements}{Declaration Statements} \subsection{Syntax} \begin{flalign*} @@ -516,7 +516,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_stmt_SDecl} \CodeSubsection{\EvalSDeclBegin}{\EvalSDeclEnd}{../Interpreter.ml} -\SectionDef[defines sequencing statements;] +\SectionDef[defines sequencing statements] {SequencingStatement}{Sequencing Statements} \hypertarget{def-sequencestatementterm}{} @@ -632,7 +632,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_stmt_SSeq} \CodeSubsection{\EvalSSeqBegin}{\EvalSSeqEnd}{../Interpreter.ml} -\SectionDef[defines call statements;] +\SectionDef[defines call statements] {CallStatements}{Call Statements} \hypertarget{def-callstatementterm}{} Call statements are used to invoke procedures and setters. @@ -704,7 +704,7 @@ \subsection{Semantics} \hypertarget{def-conditionalstatementterm}{} -\SectionDef[defines conditional statements;] +\SectionDef[defines conditional statements] {ConditionalStatements}{Conditional Statements} A conditional statement evaluates its \texttt{then} statement list if the condition expression evaluates to $\True$. If the condition expression @@ -813,7 +813,7 @@ \subsection{Semantics} \CodeSubsection{\EvalSCondBegin}{\EvalSCondEnd}{../Interpreter.ml} \hypertarget{def-casestatementterm}{} -\SectionDef[defines case statements;] +\SectionDef[defines case statements] {CaseStatements}{Case Statements} Case statements allow executing different statements, based on which condition an expression satisfies. @@ -1187,7 +1187,7 @@ \subsection{Semantics} \ASLListing{Evaluating case alternative sub-expressions}{CaseStatement.where}{\definitiontests/CaseStatement.where.asl} \hypertarget{def-assertionstatementterm}{} -\SectionDef[defines assertion statements;] +\SectionDef[defines assertion statements] {AssertionStatements}{Assertion Statements} Assertion statements are used to check that certain conditions are satisfied. They take a single \booleantypeterm{} operand, which we refer to as the @@ -1254,7 +1254,7 @@ \subsection{Semantics} \CodeSubsection{\EvalSAssertBegin}{\EvalSAssertEnd}{../Interpreter.ml} -\SectionDef[defines while statements;] +\SectionDef[defines while statements] {WhileStatements}{While Statements} \hypertarget{def-whilestatementterm}{} @@ -1435,7 +1435,7 @@ \subsection{Semantics} \RenderProseAndFormally{tick_loop_limit} -\SectionDef[defines repeat statements;] +\SectionDef[defines repeat statements] {RepeatStatements}{Repeat Statements} \hypertarget{def-repeatstatementterm}{} @@ -1504,7 +1504,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_stmt_SRepeat} \CodeSubsection{\EvalSRepeatBegin}{\EvalSRepeatEnd}{../Interpreter.ml} -\SectionDef[defines for-looping statements;] +\SectionDef[defines for-looping statements] {ForStatements}{For Statements} \hypertarget{def-forstatementterm}{} @@ -1680,7 +1680,7 @@ \subsection{Semantics} \RenderProseAndFormally{eval_for_step} \hypertarget{def-throwstatementterm}{} -\SectionDef[defines throw statements;] +\SectionDef[defines throw statements] {ThrowStatements}{Throw Statements} \subsection{Syntax} \begin{flalign*} @@ -1722,7 +1722,7 @@ \subsection{Semantics} \CodeSubsection{\EvalSThrowBegin}{\EvalSThrowEnd}{../Interpreter.ml} \hypertarget{def-trystatementterm}{} -\SectionDef[defines try statements;] +\SectionDef[defines try statements] {TryStatements}{Try Statements} \subsection{Syntax} \begin{flalign*} @@ -1815,7 +1815,7 @@ \subsection{Semantics} \CodeSubsection{\EvalSTryBegin}{\EvalSTryEnd}{../Interpreter.ml} \hypertarget{def-returnstatementterm}{} -\SectionDef[defines return statements;] +\SectionDef[defines return statements] {ReturnStatements}{Return Statements} \subsection{Syntax} \begin{flalign*} @@ -1901,7 +1901,7 @@ \subsection{Semantics} \RenderProseAndFormally{write_folder} \hypertarget{def-printstatementterm}{} -\SectionDef[defines print statements;] +\SectionDef[defines print statements] {PrintStatements}{Print Statements} \subsection{Syntax} \begin{flalign*} @@ -2065,7 +2065,7 @@ \subsection{Semantics} } \end{mathpar} -\SectionDef[defines the unreachable statement;] +\SectionDef[defines the unreachable statement] {UnreachableStatement}{The Unreachable Statement} \hypertarget{def-unreachablestatementterm}{} \listingref{UnreachableStatement} shows an example of using an \unreachablestatementterm{} diff --git a/asllib/doc/SubprogramCalls.tex b/asllib/doc/SubprogramCalls.tex index 52adf51e91..d57f570c01 100644 --- a/asllib/doc/SubprogramCalls.tex +++ b/asllib/doc/SubprogramCalls.tex @@ -17,7 +17,7 @@ \chapter{Subprogram Calls\label{chap:SubprogramCalls}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for subprogram calls;]{Subprogram Calls} +\FormalRelationsDef[defines the formal relations for subprogram calls]{Subprogram Calls} \paragraph{Syntax:} Subprogram calls are grammatically derived from $\Nexpr$ and $\Nstmt$. \paragraph{Abstract Syntax:} Subprogram calls are derived in the abstract syntax by $\ECall$ and $\SCall$; @@ -25,7 +25,7 @@ \chapter{Subprogram Calls\label{chap:SubprogramCalls}} \paragraph{Semantics:} Subprogram calls are evaluated by $\evalcall$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef[defines the syntax of subprogram calls;]{Subprogram Calls} +\SyntaxDef[defines the syntax of subprogram calls]{Subprogram Calls} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{flalign*} \Nexpr \derives\ & \Tidentifier \parsesep \PlistZero{\Nexpr} &\\ @@ -33,7 +33,7 @@ \chapter{Subprogram Calls\label{chap:SubprogramCalls}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef[defines the abstract syntax of subprogram calls;]{Subprogram Calls} +\AbstractSyntaxDef[defines the abstract syntax of subprogram calls]{Subprogram Calls} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RenderTypes[remove_hypertargets]{calls} diff --git a/asllib/doc/SubprogramDeclarations.tex b/asllib/doc/SubprogramDeclarations.tex index 0b8df750e4..fc69ace6ea 100644 --- a/asllib/doc/SubprogramDeclarations.tex +++ b/asllib/doc/SubprogramDeclarations.tex @@ -16,7 +16,7 @@ \chapter{Subprogram Declarations\label{chap:SubprogramDeclarations}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SectionDef[discusses \emph{accessors};] +\SectionDef[discusses \emph{accessors}] {Accessors}{Accessors} Special kinds of subprograms are \emph{getters} and \emph{setters}, which are paired to form an \emph{accessor} declaration. Intuitively, an accessor is used to abstract reading and writing to a global storage datatype. @@ -28,7 +28,7 @@ \chapter{Subprogram Declarations\label{chap:SubprogramDeclarations}} \ASLListing{An accessor declaration}{AccessorDeclaration}{\definitiontests/Accessor.asl} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for subprogram declarations;]{Subprogram Declarations} +\FormalRelationsDef[defines the formal relations for subprogram declarations]{Subprogram Declarations} \paragraph{Syntax:} Subprogram declarations are grammatically derived from $\Ndecl$ via the subset of productions shown in \SyntaxRef{Subprogram Declarations}. @@ -40,7 +40,7 @@ \chapter{Subprogram Declarations\label{chap:SubprogramDeclarations}} \paragraph{Semantics:} The dynamic semantics of subprogram calls is given in \chapref{SubprogramCalls}. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef[defines the syntax of subprogram declarations;]{Subprogram Declarations} +\SyntaxDef[defines the syntax of subprogram declarations]{Subprogram Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RequirementDef{NoEmptyBody} diff --git a/asllib/doc/SymbolicEquivalenceTesting.tex b/asllib/doc/SymbolicEquivalenceTesting.tex index 13f8c5ab01..91a6f10ecf 100644 --- a/asllib/doc/SymbolicEquivalenceTesting.tex +++ b/asllib/doc/SymbolicEquivalenceTesting.tex @@ -26,7 +26,7 @@ \chapter{Symbolic Reduction and Equivalence Testing\label{chap:SymbolicEquivalen \ChapterOutline -\SectionDef[formally defines equivalence for expressions, types, constraints, and bitfields;] +\SectionDef[formally defines equivalence for expressions, types, constraints, and bitfields] {Equivalence Definitions}{Equivalence Definitions} \begin{definition}[Expression Equivalence] \hypertarget{def-equivalentexprsterm}{} diff --git a/asllib/doc/Syntax.tex b/asllib/doc/Syntax.tex index df7599cb81..ffa4272c42 100644 --- a/asllib/doc/Syntax.tex +++ b/asllib/doc/Syntax.tex @@ -97,7 +97,7 @@ \section*{Resolving ambiguities: conflicts, token priorities, and associativitie \ChapterOutline -\SectionDef[defines \emph{inlined derivations};] +\SectionDef[defines \emph{inlined derivations}] {InlinedDerivations}{Inlined Derivations} Context-free grammars consist of a list of \emph{derivations} $N \derives \KleeneStar{S}$ where $N$ is a non-terminal symbol and $S$ is a list of non-terminal symbols and terminal symbols, @@ -149,7 +149,7 @@ \section*{Resolving ambiguities: conflicts, token priorities, and associativitie Barring mutually-recursive derivations involving inlined derivations, it is possible to expand all inlined derivations to obtain a context-free grammar without any inlined derivations. -\SectionDef[defines \emph{parametric productions};] +\SectionDef[defines \emph{parametric productions}] {ParametricProductions}{Parametric Productions} A parametric production has the form $N(p_{1..m}) \derives R_1 \;|\; \ldots \;|\; R_k$ @@ -257,7 +257,7 @@ \section*{Resolving ambiguities: conflicts, token priorities, and associativitie \TClistZero{x} \derives \ & \option{\TClistOne{x}} &\\ \end{flalign*} -\SectionDef[defines the ASL grammar;] +\SectionDef[defines the ASL grammar] {ASLGrammar}{ASL Grammar} We now present the list of derivations for the ASL Grammar where the start non-terminal is $\Nspec$. % @@ -677,7 +677,7 @@ \section*{Resolving ambiguities: conflicts, token priorities, and associativitie |\ & \Tor \;|\; \Trdiv \;|\; \Tshl \;|\; \Tshr \;|\; \Tpow \;|\; \Tcoloncolon \;|\; \Tplusplus \end{flalign*} -\SectionDef[defines parse trees;] +\SectionDef[defines parse trees] {ParseTrees}{Parse Trees} We now define \emph{parse trees} for the ASL expanded grammar. Those are later used to build Abstract Syntax Trees. diff --git a/asllib/doc/TopLevel.tex b/asllib/doc/TopLevel.tex index cab81d9c5b..f9026c6b64 100644 --- a/asllib/doc/TopLevel.tex +++ b/asllib/doc/TopLevel.tex @@ -17,7 +17,7 @@ \chapter{Top Level\label{chap:TopLevel}} \ChapterOutline -\SectionDef[presents an example of how to construct an ASL interpreter;] +\SectionDef[presents an example of how to construct an ASL interpreter] {Example Interpreter}{Example Interpreter} \NotImportedToASLSpecYet{ \hypertarget{def-checkandinterpret}{} diff --git a/asllib/doc/TypeAttributes.tex b/asllib/doc/TypeAttributes.tex index e932c79b3c..709eda663d 100644 --- a/asllib/doc/TypeAttributes.tex +++ b/asllib/doc/TypeAttributes.tex @@ -1,5 +1,5 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SectionDef[defines predicates for classifying types and functions for inspecting their structure;] +\SectionDef[defines predicates for classifying types and functions for inspecting their structure] {BasicTypeAttributes}{Basic Type Attributes} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/asllib/doc/TypeDeclarations.tex b/asllib/doc/TypeDeclarations.tex index 3048d7e843..91dc05e25f 100644 --- a/asllib/doc/TypeDeclarations.tex +++ b/asllib/doc/TypeDeclarations.tex @@ -7,7 +7,7 @@ \chapter{Type Declarations\label{chap:TypeDeclarations}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for type declarations;]{Type Declarations} +\FormalRelationsDef[defines the formal relations for type declarations]{Type Declarations} \paragraph{Syntax:} Type declarations are grammatically derived from $\Ndecl$. \paragraph{Abstract Syntax:} Type declarations are derived in the abstract syntax from $\decl$, and generated by $\builddecl$ (see \ASTRuleRef{TypeDecl}). @@ -15,7 +15,7 @@ \chapter{Type Declarations\label{chap:TypeDeclarations}} \paragraph{Semantics:} Type declarations have no associated dynamic semantics. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SyntaxDef[defines the syntax for type declarations;]{Type Declarations} +\SyntaxDef[defines the syntax for type declarations]{Type Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{flalign*} \Ndecl \derives \ & \Ttype \parsesep \Tidentifier \parsesep \Tof \parsesep \Ntydecl \parsesep \Tsemicolon&\\ @@ -26,7 +26,7 @@ \chapter{Type Declarations\label{chap:TypeDeclarations}} \end{flalign*} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\AbstractSyntaxDef[defines the abstract syntax for type declarations;]{Type Declarations} +\AbstractSyntaxDef[defines the abstract syntax for type declarations]{Type Declarations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \RenderTypes[remove_hypertargets]{decl_type} diff --git a/asllib/doc/TypeDomains.tex b/asllib/doc/TypeDomains.tex index fb04727852..5b46d90eab 100644 --- a/asllib/doc/TypeDomains.tex +++ b/asllib/doc/TypeDomains.tex @@ -1,5 +1,5 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\SectionDef[defines the semantics of types by associating a value to each type;] +\SectionDef[defines the semantics of types by associating a value to each type] {DomainOfValuesForTypes}{Domain of Values for Types} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% This section formalises the concept of the set of values for a given type. diff --git a/asllib/doc/Types.tex b/asllib/doc/Types.tex index 048020663b..74486a9bfb 100644 --- a/asllib/doc/Types.tex +++ b/asllib/doc/Types.tex @@ -14,7 +14,7 @@ \chapter{Types\label{chap:Types}} \ChapterOutline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\FormalRelationsDef[defines the formal relations for types;]{Types} +\FormalRelationsDef[defines the formal relations for types]{Types} \paragraph{Syntax:} \Anonymoustypes{} are grammatically derived from $\Nty$ and types that must be declared and named are grammatically derived from $\Ntydecl$; @@ -98,7 +98,7 @@ \chapter{Types\label{chap:Types}} \end{mathpar} \hypertarget{integertypeterm}{} -\SectionDef[defines the \integertypeterm{};] +\SectionDef[defines the \integertypeterm{}] {IntegerTypes}{Integer Types} The \emph{\integertypesterm{}} represent the mathematical integer values. @@ -344,7 +344,7 @@ \subsection{Typing Integer Types\label{sec:TypingIntegerTypes}} \RenderProseAndFormally{annotate_constraint} -\SectionDef[defines the \realtypeterm{};] +\SectionDef[defines the \realtypeterm{}] {RealType}{The Real Type} \hypertarget{realtypeterm}{} The \emph{\realtypeterm{}} represents mathematical rational number values. @@ -388,7 +388,7 @@ \subsection{Typing the Real Type\label{sec:TypingRealType}} \RenderProseAndFormally{annotate_type_t_real} \CodeSubsection{\TRealBegin}{\TRealEnd}{../Typing.ml} -\SectionDef[defines the \stringtypeterm{};] +\SectionDef[defines the \stringtypeterm{}] {StringType}{The String Type} \hypertarget{stringtypeterm}{} \hypertarget{stringtypesterm}{} @@ -428,7 +428,7 @@ \subsection{Typing the String Type\label{sec:TypingStringType}} \RenderProseAndFormally{annotate_type_t_string} \CodeSubsection{\TStringBegin}{\TStringEnd}{../Typing.ml} -\SectionDef[defines the \booleantypeterm{};] +\SectionDef[defines the \booleantypeterm{}] {BooleanType}{The Boolean Type} \hypertarget{booleantypeterm}{} The \emph{\booleantypeterm{}} represents Booleans. @@ -462,7 +462,7 @@ \subsection{Typing the Boolean Type\label{sec:TypingBooleanType}} \RenderProseAndFormally{annotate_type_t_bool} \CodeSubsection{\TBoolBegin}{\TBoolEnd}{../Typing.ml} -\SectionDef[defines the \bitvectortypeterm{};] +\SectionDef[defines the \bitvectortypeterm{}] {BitvectorTypes}{Bitvector Types} \hypertarget{bitvectortypeterm}{} \emph{Bitvectors} represent sequences of $0$ and $1$ bits ordered according to \RequirementRef{BitvectorOrdering}. @@ -602,7 +602,7 @@ \subsection{Typing Bitvector Types} \RenderProseAndFormally{annotate_type_t_bits} \CodeSubsection{\TBitsBegin}{\TBitsEnd}{../Typing.ml} -\SectionDef[defines \Tupletypesterm{};] +\SectionDef[defines \Tupletypesterm{}] {TupleTypes}{Tuple Types} \hypertarget{tupletypeterm}{} @@ -671,7 +671,7 @@ \subsection{Typing Tuple Types\label{sec:TypingTupleTypes}} \RenderProseAndFormally{annotate_type_t_tuple} \CodeSubsection{\TTupleBegin}{\TTupleEnd}{../Typing.ml} -\SectionDef[defines parenthesised types;] +\SectionDef[defines parenthesised types] {ParenthesisedTypes}{Parenthesised Types} A single type inside parentheses is not considered to be a tuple, but rather the element inside the parenthesis. @@ -697,7 +697,7 @@ \subsection{Abstract Syntax} } \end{mathpar} -\SectionDef[defines \Enumerationtypesterm{};] +\SectionDef[defines \Enumerationtypesterm{}] {EnumerationTypes}{Enumeration Types} \hypertarget{enumerationtypeterm}{} The \emph{\enumerationtypeterm} defines a list of enumeration literals, @@ -772,7 +772,7 @@ \subsection{Typing Enumeration Types\label{sec:TypingEnumerationTypes}} \RenderProseAndFormally{annotate_type_t_enum_decl} \CodeSubsection{\TEnumDeclBegin}{\TEnumDeclEnd}{../Typing.ml} -\SectionDef[defines array types;] +\SectionDef[defines array types] {ArrayTypes}{Array Types} \hypertarget{arraytypeterm}{} % @@ -867,7 +867,7 @@ \subsection{Typing Array Types\label{sec:TypingArrayTypes}} \RenderProseAndFormally{check_underlying_integer} \CodeSubsection{\CheckUnderlyingIntegerBegin}{\CheckUnderlyingIntegerEnd}{../Typing.ml} -\SectionDef[defines record types;] +\SectionDef[defines record types] {RecordTypes}{Record Types} \hypertarget{recordtypeterm}{} % @@ -908,7 +908,7 @@ \subsection{Typing Record Types\label{sec:TypingRecordTypes}} \RenderProseAndFormally{annotate_type_t_record_exception} \CodeSubsection{\TStructuredDeclBegin}{\TStructuredDeclEnd}{../Typing.ml} -\SectionDef[defines exception types;] +\SectionDef[defines exception types] {ExceptionTypes}{Exception Types} \hypertarget{exceptiontypeterm}{} An exception is a \structuredtypeterm{} consisting of a list of field identifiers @@ -947,7 +947,7 @@ \subsection{Abstract Syntax} \subsection{Typing Exception Types} The rule for typing exception types is \TypingRuleRef{TStructuredDecl}. -\SectionDef[defines collection types;] +\SectionDef[defines collection types] {CollectionTypes}{Collection Types} \hypertarget{collectiontypeterm}{} @@ -997,7 +997,7 @@ \subsection{Typing Collection Types} \RenderProseAndFormally{annotate_type_t_collection} -\SectionDef[defines named types;] +\SectionDef[defines named types] {NamedTypes}{Named Types} A named type declaration allows declaring a new type associated with the given name. The intent is that, by default, any named type should not be assignable to or from any other named type, even @@ -1056,7 +1056,7 @@ \subsection{Typing Named Types\label{sec:TypingNamedTypes}} \RenderProseAndFormally{annotate_type_t_named} \CodeSubsection{\TNamedBegin}{\TNamedEnd}{../Typing.ml} -\SectionDef[defines \emph{declared types} and restrictions over them;] +\SectionDef[defines \emph{declared types} and restrictions over them] {DeclaredTypes}{Declared Types} A declared type can be an \enumerationtypeterm{}, a \recordtypeterm, an \exceptiontypeterm, or an \anonymoustype. \subsection{Syntax} diff --git a/asllib/doc/macros.hva b/asllib/doc/macros.hva index 855a5d7352..9369087c2e 100644 --- a/asllib/doc/macros.hva +++ b/asllib/doc/macros.hva @@ -160,10 +160,10 @@ \newtokens{\csname ASLChapterOutlineSubsections@#1@#2\endcsname}% }{}% \addtokens{\csname ASLChapterOutlineSubsections@#1@#2\endcsname} - {\item \secref{#3} #4}} + {\item \secref{#3} #4;}} \newcommand{\my@ASLChapterOutlineSection}[3]{% - \item \secref{#2} #3% + \item \secref{#2} #3;% \@ifundefined{ASLChapterOutlineSubsections@#1@#2}{}{% \begin{itemize}% \csname ASLChapterOutlineSubsections@#1@#2\endcsname