coding_standards.tex

%! program = pdflatexmk

% Free & Fair Coding Standards
% Copyright (C) 2024 Free & Fair

\documentclass[10pt,letter]{article}

%%% PACKAGES
\usepackage[in]{fullpage}
\usepackage{tabularray}
\usepackage[pdftex,bookmarks,colorlinks,breaklinks]{hyperref}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{listings}
\usepackage{verbatim}
\usepackage{lmodern}
\usepackage[T1]{fontenc}
\setlength {\marginparwidth}{2cm} 
\usepackage{todonotes}
\usepackage{enumitem}
\hypersetup{linkcolor=blue,citecolor=blue,filecolor=black,urlcolor=blue} 
\parindent 0pt
\textheight 9in
\topmargin 0in
\setlength{\parskip}{10pt plus 1pt minus 1pt}

\usepackage{tocloft} 
\setlength\cftparskip{2pt} 

\renewcommand{\subsectionautorefname}{section}
\renewcommand{\subsubsectionautorefname}{section}

\pagestyle{empty}

%%% BEGIN DOCUMENT
\begin{document}

\begin{center}
{\Large \textbf{Free \& Fair Coding Standards}}
\end{center}
\vspace{-6pt}

\textit{Adapted by Free \& Fair from the KindSoftware Coding Standards} \hspace{\fill} \textit{Version 1.0} \\
\textit{and other offshoots of the original Infospheres Java Coding Standard} \hspace{\fill} \textit{December 2024}

\vspace{-12pt}

\rule{\textwidth}{1pt}

\tableofcontents

\section{Introduction}

Code standards aren't just about obsession, they are about productivity, professionalism, and presentation.
The predecessors to this code standard have been used by several companies, research groups, and numerous individuals including industrial teams at \href{https://www.sun.com/}{Sun Microsystems}, DALi, Fulcrum Microsystems, \href{https://galois.com}{Galois}, and \href{https://certik.com}{CertiK}; the Compositional Computing/Infospheres Group in the Department of Computer Science at \href{https://www.caltech.edu/}{Caltech}; the Security of Systems (SoS) Group in the \href{https://www.ru.nl/en/institute-for-computing-and-information-sciences}{Nijmegen Institute for Computing and Information Science} at the \href{https://www.ru.nl/}{Radboud University Nijmegen}; the KindSoftware: Software Engineering with Applied Formal Methods Group in the \href{https://www.ucd.ie/cs/}{School of Computer Science and Informatics} at \href{https://www.ucd.ie/}{University College Dublin}; the Applied Formal Methods Group in the \href{https://www.tacoma.uw.edu/set}{Institute of Technology} at the \href{https://tacoma.uw.edu}{University of Washington Tacoma}; and students in applied formal methods and introductory programming courses at all the schools listed above and \href{https://www.hmc.edu}{Harvey Mudd College}.

Many people helped with the evolution of this code standard. These practices were not created in a vacuum. They are tried and true rules that have been used to produce both research and commercial systems by teams of dozens of programmers. The resulting products (student assignments, government research project deliverables, open-source projects, internal company tooling, etc.) are readable, maintainable, robust, testable, and professional.

While not all the rules are applicable to every developer or all systems, a general adherence to the rules and a belief in software engineering practices often results in happier and healthier developers and systems.

In the context of this document, ``structure'' means ``organization, look, and feel'' of a body of code. It includes elements of system and subsystem organization (packages), documentation (feature documentation, structured documentation tags such as Javadoc or docstrings, inline comments, and index files), specification (inline and external specifications, running comments, index files), and development (code organization). Adhering to these standards means that every piece of code has the same structure so that a reader can instantly know where to find a piece of information (attribute, import, method, feature, etc.) without having to search through an entire source file.

\section{Documentation}

Documentation is all about communication. If you have any hope or desire to see your code understood and reused, it needs to be comprehensively documented. We use various tools to evaluate the true comment volume of code, depending on implementation language. For most languages a minimal acceptable documentation ratio is about 35\%, but we really look for ratios around 50\%.

These numbers sound high even for extensively documented classroom code, and \emph{incredibly} high for Open Source Software. So where does all this documentation come from?
In-code documentation isn't all that counts toward the ratio. Overviews, design documents, manpages, etc. all contribute as well.

In our experience, once you document a system so that other programmers can both rapidly understand what you have built and be capable of building it from scratch with your design, you will have ratios close to what we have prescribed.

\paragraph{How much is enough?}

Your guiding metric for ``How much is enough?'' should be the following: Communicate exactly enough information in your comments so that the reader can implement what you are describing, correctly.
Quality is better than quantity. Comments that convey no information about the choices made during design or coding, or are overly verbose, are generally not helpful. For example, if a component that can be accessed externally has a variable called \texttt{accessCount} that tracks the number of times it is accessed, a useful comment at that variable’s declaration might be ``The number of external accesses.'' By contrast, a comment stating ``This variable is called \texttt{accessCount} because it counts the number of external accesses and we wanted to name it in a way that made that meaning clear to the eventual reader of this code.'' serves primarily to artificially increase the comment/code ratio. 

\paragraph{Self-documenting code}

Some argue that code should be ``self-documenting''. This is true in some sense, and we enforce it in some ways through naming conventions and running comments, but it isn't enough. What about the reader who doesn't know the language you are coding in? What about proprietary reusable components? Obviously, something more is necessary.
We find this opinion especially among the functional programming languages community. It astounds and confuses us that such a bright group of programmers can seriously think that no documentation is better than good documentation. We're working to make a difference there as well.

\paragraph{Real coders don't document}

Also, for those of you that think that documentation is for weaklings and that real hackers, Masters, and Rambo-coders don't need comments; believe us, we could find some code that you wouldn't understand even with days of head-scratching (if you're in the area, drop by and we'll prove it). Rambo-coders need not apply.
\subsection{Comment Types}
We use \textit{semantic properties} to document program code in regular, parseable, meaningful ways.
Each property has a legal scope of use, called its \textit{context}. Contexts are defined in a coarse, language-independent fashion using inclusion operators in kind theory. Contexts are comprised of \textit{files}, \textit{modules}, \textit{features}, and \textit{variables}.
\textit{Files} are exactly that: data files in which program code resides. The scope of a file encompasses everything contained in that file.
A \textit{module} is some large-scale program unit. Modules are typically realized by an explicit module- or class-like structure. Examples of modules are classes in object-oriented systems, modules in languages of the Modula and ML families, packages in the Ada lineage, etc. Other words and structures typically bound to modules include units, protocols, interfaces, etc.
\textit{Features} are the entry point for computation. Features are often named, have parameters, and return values. Functions and procedures in structured languages are features, as are methods in object-oriented languages, and functions in functional languages.
Finally, \textit{variables} are program variables, attributes, constants, enumerations, etc. Because few languages enforce any access principles for variables, variables can vary in semantics considerably.
We maintain regular conventions for property-based documentation for each of these scopes. They are documented in the next few sections.

\subsubsection{File Comment}

Every file has a file comment containing at least the following information (example below):

\begin{enumerate}
  \item The title of the project with which the file is associated, using the \texttt{title} property.
  \item A short description of the file's contents, using the \texttt{description} property.
  \item Any copyright information relevant to the project, using the \texttt{copyright} property.
  \item The license(s) under which the file is protected, using the \texttt{license} property.
  \item The primary authors of the file, using the \texttt{author} property.
  \item The version of the file, using the \texttt{version} property. 
\end{enumerate}

\subsubsection{Module Comment}

A module (class, interface, package, module, unit, protocol, etc.) comment describes the purpose of the module, guaranteed invariants, usage instructions, and/or usage examples. The beginning of the comment should be a description of the module in exactly one sentence. Also included in the class comment are any reminders or disclaimers about required or desired improvements. See the below chart for appropriate properties and usages.
Each module comment block must include exactly one \texttt{version} property and at least one \texttt{author} property. The \texttt{author} properties often list everyone who has written more than a few lines of the class. Each \texttt{author} property should list exactly one author. The \texttt{version} property's version is a project specific string (e.g. ``1.0b5c7''), preferably following \href{https://semver.org/}{semantic versioning} conventions. Additionally, each module may optionally contain a single-line comment at the end stating that the module declaration has ended.

\subsubsection{Feature Comment}

Use language and local documentation conventions to describe every feature’s nature, purpose, specification, effects, algorithmic notes, usage instructions, reminders, etc. The beginning of a feature comment should be a summary of the feature in exactly one sentence using the \todo{property name here} TODO property. See the chart below for appropriate properties and usages.

\subsubsection{Variable Comment}

At minimum, variables should be commented with those semantic properties that are not implicitly specified by program structure. Many variable-scoped semantic properties are implicit within the structure of the program code given the semantics of the programming language in use. For example, the \texttt{hides} property, when used, is explicit documentation of an implicit feature of the language. Thus, the most important semantic property to use on variables is the \texttt{values} property, which should also be documented as a class invariant.

\section{Naming Conventions}

You can name temporary and loop variables anything you like. We suggest prefixes of ``temp'' for temporary variables and ``loop'' for loop indices.

All other constructs, especially types and attributes of your objects and parameters of modules, must have \textit{some} uniform naming scheme. Different programming languages have different standard conventions, and different engineering teams have their own standard conventions for various languages; we specify some details in the specific language sections near the end of this document.

In general, all variable names should have semantic value. They should not be bound to type or class since that might change over time but the semantics will (should) not.

\section{Semantic Properties}

\textit{Semantic properties} (or just ``properties'' for short) are our generic way of talking about special purpose documentation used to ``tag'' program structures. Examples of documentation properties include Javadoc tags and Eiffel indexing properties. Thus, if you are a Java programmer, read ``property'' as ``tag''; if you are an Eiffel programmer read it as ``index property'' and ``well-structured comment''.
Semantic properties are discussed in two papers: \href{https://www.arxiv.org/abs/cs.SE/0204035}{Semantic Properties for Lightweight Specification in Knowledgeable Development Environments} and \href{https://www.arxiv.org/abs/cs.SE/0204036}{Semantic Component Composition}.

Property values that are strings should be enclosed in double-quotes (''). Strings that are split across lines should use a backslash ($\backslash$) as a continuation character. See the example files and headers for examples.
In all of the following properties, Expression means (predicate | code segment | natural language description). A predicate is a boolean-valued function. Examples of valid predicates for detailed specification purposes include expressions written in specification languages like Formal \href{https://www.bon-method.com/}{BON}, \href{https://www.jmlspecs.org/}{JML}, \href{https://frama-c.com/html/acsl.html}{ACSL}, \href{https://cryptol.net/}{Cryptol}, \href{https://galois.com/project/gumbo/}{GCL}, and \href{https://www.omg.org/spec/OCL/}{OCL}, or traditional predicates in any normal (predicate) calculus or (boolean, Hoare) logic. A code segment is a legal expression from any programming language, but is most often written in the language of the code it documents. A natural language description is a description written in a spoken language (like English).

For all properties, entities enclosed in () or <> must be so enclosed when using the properties. That is, ``(Expression)'' means literally ``('' + the expression + ``)''. Entities enclosed in [ ] in the table are optional, and should not be enclosed in literal square brackets when present.
The table lists, in the ``Usage'' column, the programmatic constructs to which each property is applicable. Possible values for this column are \textit{files}, \textit{modules}, \textit{features}, \textit{variables}, \textit{all}, and \textit{special}. Special usages are explained in the ``Purpose/Description'' column. We provide a map of these constructs to each programming language for which we go into greater detail later in this document.

\subsection{Property Conventions}

The following table documents all properties and their usages.

\begin{longtblr}{colspec={||Q[m,wd=1.6in]|Q[m,wd=0.55in]|Q[m,wd=3.85in]||}, rowhead=1, cells={font=\fontsize{9pt}{10pt}\selectfont}}
\hline
\textbf{Property} & \textbf{Usage} & \textbf{Purpose/Description} \\ \hline
\SetCell[c=3]{c} \textbf{\textit{Meta-Information}} \\* \hline
% -------
\texttt{author Full\_name} & Modules & Lists an author of the module. The text has no special internal structure. A doc comment may contain multiple \texttt{author} properties. A standard \texttt{author} property includes only the full name of the author and should not include other information (like an email address, web page, etc.) unless absolutely necessary. \\ \hline
% -------
{\texttt{refines URL [fully resolved name]} or \\ \texttt{refines Document\_name [Version]}} & Modules, Features & Points to the refinement(s) of this construct, typically via a Git URL plus the fully resolved name of the associated construct.  Alternatively, refers to a relevant document (preferably with a version number) by name. \\ \hline
% -------
\texttt{bug Description} & Modules, Features & Describes a known bug in the module or feature. One property should be used for each bug. If a construct has a known bug, it should be described. Omission of a bug description is considered as bad an offense as the existence of the bug in the first place. \\ \hline
% -------
\texttt{copyright Copyright} & Files & Indicates the holders of copyright in the file. \\ \hline
% -------
\texttt{description Description} & Modules, Features, Files & A brief description of a construct. In the case of a module or feature, this should be a one-sentence summary of the construct; in the case of a file, it can be longer.  This sentence is meant to correspond to a Lando indexing clause for the construct. \\ \hline
% -------
\texttt{history Description} & All & Describes how a feature has been significantly modified over time. For each major change, the description should include: who made it, when it was made (date and version), what was done, why it was done, and a reference to the change request and/or user requirement that resulted in the change being made. \\ \hline
% -------
\texttt{license License} & Files & Indicates the license(s) under which the file is made available. \\ \hline
% -------
\texttt{title Title} & Files & Documents the title of the project with which the file is associated. \\ \hline
% -------
\SetCell[c=3]{c} \textbf{\textit{Pending Work}} \\* \hline
% -------
\texttt{idea Author [Classifier] - Description} & All & Describes an idea for something from the named author. The optional \texttt{Classifier} argument is for ad hoc categorization of ideas. Typical examples include optimizations, algorithmic changes, etc. \\ \hline
% -------
\texttt{review Reviewer - Description} & All & Indicates to a reader that a particular block of code still needs to be reviewed (by the named reviewer) for some reason. Typical reasons include the ``something's not right here'' syndrome, boundary condition checks, not understanding an algorithm completely, etc. \\ \hline
% -------
\texttt{todo Author - Description} & All & Describes some work that still needs to be accomplished by the named author. Typical examples include optimizing algorithms, proving correctness of new code, renaming variables or features to conform to standards, cleaning up code, etc. \\ \hline
% -------
\SetCell[c=3]{c} \textbf{\textit{Formal Specifications}} \\* \hline
% -------
\texttt{[label:] ensures (Expression) [<Exception> -] Description} & Features & Describes a postcondition that holds after a feature has completed successfully. If a postcondition is violated, then \texttt{Exception} (if specified) is raised. One property is used for each postcondition. Note that no requirement is made on the visibility of postconditions, so these are often used as the private, development specifications of a feature. The visibility of a postcondition is exactly the visibility of the feature to which it is bound. Acceptable synonyms for \texttt{ensures} are \texttt{ensure}, \texttt{postcondition}, and \texttt{post}. \\ \hline
% -------
\texttt{generate (Expression) [Description]} & Modules, Features & Describes new, possibly unreferenced, entities (for example, new threads of control) created as a result of the execution of a feature or the instantiation of a module. \\ \hline
% -------
\texttt{invariant (Expression) [<Exception>] Description} & Modules, Features & Specifies a module or feature invariant. An invariant is a predicate (Boolean expression) that must hold whenever the entity being described is in a stable state. \texttt{Expression} must, therefore, evaluate to a Boolean.
An object is defined as being in a stable state when either (a) no threads of control are within the object or operating upon the object, (b) a single thread of control is about to enter a feature of the object, or (c) a single thread of control is about to exit a feature of the object.
If an invariant is violated when an object is in a stable state, \texttt{Exception} (if specified) is raised. \\ \hline
% -------
\texttt{modify (SINGLE-ASSIGNMENT | QUERY | Expression) Description} & All & Indicates the semantics of a construct as follows:
{\\ \texttt{SINGLE-ASSIGNMENT} indicates that the construct will be set or operated upon exactly once. Once the variable is set or the feature is called, it will never be set or called again.
\\ \texttt{QUERY} indicates that the construct is read-only and has no side-effects.
\\ \texttt{Expression} indicates that a feature modifies an object and describes how it does so.} \\ \hline
% -------
\texttt{[label:] requires (Expression) [<Exception> -] [Description]} & Features & Describes a precondition that must hold before the feature can be safely invoked. One property is used for each precondition. If a precondition is violated then \texttt{Exception} (if specified) is raised. The visibility of preconditions follows the same rules as the visibility of postconditions. Acceptable synonyms for \texttt{requires} are \texttt{require}, \texttt{precondition}, and \texttt{pre}. \\ \hline
% -------
\SetCell[c=3]{c} \textbf{\textit{Concurrency Control}} \\* \hline
% -------
\texttt{concurrency (SEQUENTIAL | GUARDED | CONCURRENT | TIMEOUT <value> <Exception> | FAILURE <Exception> | SPECIAL) [Description]} & Modules, Features & Describes the concurrency strategy and/or approach taken by (necessary for) the module or feature. The execution context for a feature should be described at this point. The meanings of the possible parameters are as follows:
{\\ \texttt{SEQUENTIAL} means that callers must coordinate so that only one call or access to the object in question may be outstanding at once. If simultaneous calls occur, the semantics and integrity of the system are not guaranteed.
\\ \texttt{GUARDED} means that multiple calls or accesses from concurrent threads may occur simultaneously to one object in question, but only one is allowed to commence; the others are blocked until the performance of the first operation is complete. This is the behavior of \texttt{synchronized} instance methods in Java.
\\ \texttt{CONCURRENT} indicates that multiple calls or accesses from concurrent threads may occur simultaneously to the object in question, and that all will proceed concurrently with correct semantics. This is the default behavior of Java methods and fields and Eiffel features.
\\ \texttt{TIMEOUT} indicates that if a call to this feature is blocked for a time period greater than or equal to \texttt{<value>}, the exception \texttt{<Exception>} will be raised. The value is specified with units.
\\ \texttt{FAILURE} means that if a call to the feature is currently underway, all additional calls will fail and the exception \texttt{<Exception>} will be raised.
\\ \texttt{SPECIAL} indicates that the feature has concurrency semantics that are not covered by the preceding cases. Make sure to explain the particulars of the feature's semantics in sufficient detail that the reader will be quite clear on your feature's unusual semantics.
\\ }
A feature lacking a concurrency property is considered \texttt{CONCURRENT}. The semantics description is optional on features that are labeled as \texttt{SEQUENTIAL} or \texttt{GUARDED}. In general, all features should have concurrency properties. \\ \hline
% -------
\SetCell[c=3]{c} \textbf{\textit{Usage Information}} \\* \hline
% -------
\texttt{param parameter-name [WHERE (Expression)] Description} & Features & Describes a feature parameter. The description may be continued on the following line(s). The expression indicates restrictions on argument values. Restrictions that result in exceptions, such as \texttt{IllegalArgumentException} in Java, should be indicated as such. In particular, it is important to indicate whether reference arguments are allowed to be \texttt{null}/\texttt{void}. There must be one \texttt{param} property for each and every parameter to the feature. \\ \hline
% -------
\texttt{return Description} & Features & Describes a feature's return value. The description may be continued on the following line(s). If the feature being documented is a simple getter feature (or similar), a \texttt{return} property is still necessary; however, in such a case, the actual feature description may be omitted since the \texttt{return} property completely describes the feature. \\ \hline
% -------
\texttt{exception ExceptionName [IF (Expression)] Description} & Features & Describes an exception that can be raised by the feature, and the circumstances under which it is raised. The guard indicates restrictions on argument values. In particular, it is important to indicate whether reference arguments are allowed to be \texttt{null}/\texttt{void}. There must be one exception property for each and every exception declared to be raised by the feature. In Java, for instance, a \texttt{RuntimeException} or \texttt{IllegalArgumentException} declared in the feature signature must be documented with this tag. It is generally a good idea to declare in the feature signature any runtime exceptions that are raised as a result of conditions controllable at compile time (such as the feature being called in the wrong system state, or a lack of sufficient range checking on passed argument values). \\ \hline
% -------
\SetCell[c=3]{c} \textbf{\textit{Versioning}} \\* \hline
% -------
\texttt{version VersionString} & Files, Modules & Denotes the version of the construct. The text has no special internal structure, though it is encouraged that version numbers follow semantic versioning guidelines. Any construct may contain at most one \texttt{version} property. The \texttt{version} property normally refers to the version of the software project that contains the construct, rather than the version of the construct itself. \\ \hline
% -------
\texttt{deprecated Reference to replacement API.} & All & Indicates that this API element should no longer be used even though it may continue to work. By convention, the text describes the API (or APIs) that replace the deprecated API. Be as specific as necessary to differentiate between overloaded or polymorphic options.
If the API is obsolete and there is no replacement, the argument to \texttt{deprecated} should be "No replacement". \\ \hline
% -------
\texttt{since version-tag} & All & Indicates the (release) version number in which this construct first appeared. This version number, like that for the version property, is usually a project-wide version number rather than a version number for the particular construct in which the documented construct appears. No \texttt{since} property is required for features that have existed since the first version of the project. \\ \hline
% -------
\SetCell[c=3]{c} \textbf{\textit{Inheritance}} \\* \hline
% -------
\texttt{hides FeatureName [Description]} & Variables & Indicates that a particular variable hides a variable in a enclosing context (e.g., a parent class or enclosing module). \\ \hline
% -------
\texttt{overrides FeatureName [Description]} & Features & Indicates that a particular feature overrides a feature in an enclosing context (e.g., a parent class or enclosing module). If the overriding feature does not either call the feature it overrides, or implement a superset of that feature's semantics, its effects must be documented (using \texttt{precondition}, \texttt{postcondition}, and \texttt{invariant} properties and the feature description, as appropriate). \\ \hline
% -------
\SetCell[c=3]{c} \textbf{\textit{Documentation}} \\* \hline
% -------
\texttt{design Description} & All & Provides information about design decisions made about the code and/or useful things to know about parts of the code. \\ \hline
% -------
\texttt{equivalent (Expression | Code Reference)} & Modules, Features & Documents convenience or specialized features that can be defined in terms of a few operations using other features. \\ \hline
% -------
\texttt{example Description} & All & Provides one or more examples of how to use a construct. \\ \hline
% -------
\texttt{see <APIName> Label} & All & { Refers the reader to other related material. Some source processors use this information to generate hyperlinked documentation. \texttt{<APIName>} can be the name of a language API or an HTML anchor.
This property is often used to reference an external document that describes pertinent business rules or information relevant to the source code being documented.
\\
The character `\#' separates the name of a module from the name of one of its features. One of several overloaded features may be selected by including a parenthesized list of argument types after the feature name. Whitespace in \texttt{<APIName>} is significant. If there is more than one argument, there must be a single blank character between the arguments. A comment may contain multiple \texttt{see} properties. } \\ \hline
% -------
\SetCell[c=3]{c} \textbf{\textit{Dependencies}} \\* \hline
% -------
\texttt{references (Expression) [Description]} & Modules, Features, Variables & Indicates that the construct references other constructs like objects, instances, files, etc. This is primarily used to highlight subtle inter-dependencies between modules, features, etc. \\ \hline
% -------
\texttt{trace 
(GitUrl, Name) [Description]} & All & Denotes a traceability relationship between the annotated artifact and another artifact with which it is related.  The nature of the relation—--refinement or equivalence—--is typically clear from context.  The optional \texttt{Description} element is provided in cases where the traceability relation’s meaning is unclear. \\ \hline
% -------
\texttt{use (Expression) [Description]} & All & Indicates exactly those elements that are utilized by this element. This property is primarily used to highlight hidden dependencies. \\ \hline
% -------
\SetCell[c=3]{c} \textbf{\textit{Miscellaneous}} \\* \hline
% -------
\texttt{guard (Expression) [Description]} & Features & Indicates that actions use guarded waits (e.g., Java’s \texttt{Object.wait()}) until the condition specified in \texttt{Expression} holds. \\ \hline
% -------
\texttt{values (Expression) [Description]} & Variables & Describes the possible values of a variable, including ranges and/or distinct values. \\ \hline
% -------
{\texttt{time-complexity (Expression) [Description]} \\ \\ \texttt{space-complexity (Expression) [Description]}} & Features & Documents the time or space complexity of a feature. \texttt{Expression} should be in big-O notation. For example, $O(n*n)$ and $O(n^2)$ are equivalent, but the second is the more common way to express quadratic complexity. The free terms of \texttt{Expression} should be documented in the description; usually, they are related directly to instance variables of the surrounding or related classes or modules. \\ \hline
% -------
\end{longtblr}

\begin{comment}
(DMZ note: I'm commenting out these sections for now, because they're really not in good shape and the tools section, in particular, is somewhat tangential to the purpose of a coding standard.)

\section{Tools}
(DMZ note: this section needs \textit{far} more revision than some of the rest)
\subsection{(X)Emacs}
The canonical summary: \textit{Emacs is the extensible, customizable, self-documenting real-time display editor.}
\textit{(Rewritten from the XEmacs home page)} Emacs is a powerful, extensible text editor with full GUI and terminal support.
Two primary supported free implementations of Emacs exist:
\begin{itemize}
  \item \href{https://www.fsf.org/}{FSF} Emacs, the Free Software Foundation's mainline Emacs implementation, and
  \item \href{https://www.xemacs.org/}{XEmacs}, a highly graphical version initially based on an early version of GNU Emacs 19 from the Free Software Foundation and since kept up to date with recent versions of that product. XEmacs stems from a collaboration of Lucid, Inc. with \href{https://www.sun.com/}{Sun Microsystems, Inc.} and the \href{https://www.cs.uiuc.edu/}{University of Illinois}, with additional support having been provided by \href{https://www.amdahl.com/}{Amdahl Corporation} and \href{https://www.altrasoft.com/}{Altrasoft}.
\end{itemize}

\textbf{Extending Emacs.} (X)Emacs is extended through the use of Emacs Lisp \textit{packages}. The primary packages we use for the development of Java are as follows. This list is by no means complete and reflects our personal biases. Some of the following summaries come directly from the info web pages for the corresponding package.
\begin{itemize}
  \item \textbf{Semantic/Bovine.} Semantic is a program for Emacs which includes, at its core, a lexer, and two compiler compilers (bovinator and wisent). Additional tools include, support for imenu, speedbar, whichfunc, eldoc, hippie-expand, and several other build in tools.\\~The core utility is the parser infrastructure which allows different types of parsers to be linked into the system. Two build in parsers include the ``bovine'' parser, and the ``wisent'' parser.
  \item \textbf{Speedbar.} Speedbar is a program for Emacs which can be used to summarize information related to the current buffer. Its original inspiration is the `explorer' often used in modern development environments, office packages, and web browsers.
  \item \textbf{EIEIO.} Summary.
  \item \textbf{AucTeX.} Summary.
  \item \textbf{Proof General.} Summary.
  \item \textbf{Emacs Library (elib).} Summary.
  \item \textbf{Tramp.} Summary.
  \item \textbf{\href{https://repose.cx/emacs/wiki}{Wiki.}} Emacs-Wiki enables you to create and use hyperlinks and simple formatting in plain text files, and to optionally publish your pages as HTML.
  \item \textbf{\href{https://www.csd.uu.se/\textasciitilde andersl/emacs.shtml}{Folding.}} This package provides a minor mode, compatible with all major editing modes, for folding (hiding) parts of the edited text or program.\\~Folding mode handles a document as a tree, where each branch is bounded by special markers `\{\{\{' and `\}\}\}'. A branch can be placed inside another branch, creating a complete hierarchical structure.
  \item \textbf{Tracker.} This mode keeps a list of projects and associated billing entity. A single project can be selected and it will be marked in a file as active until a new command is made to stop it. A project is automatically terminated when emacs exits. If somehow this fails, the tracking data file is touched at regular intervals, so the next time the tracker is started if there is an open project a reasonable guess can be made as to when to mark it as closed. Each session can have multiple comments associated with it, in which you can mark accomplishments or whatever. It will generate informal daily summary reports and a report of total hours for a particular billee.
  \item \textbf{Calendar and Diary.} Emacs provides the functions of a desk calendar, with a diary of planned or past events. It also has facilities for managing your appointments, and keeping track of how much time you spend working on certain projects.
  \item \textbf{ECB (Emacs Code Browser).} While (X)Emacs already has good \textit{editing} support for many modes, its \textit{browsing} support is somewhat lacking. That's where ECB comes in: it displays a number of informational windows that allow for easy source code navigation and overview.
  \item \textbf{Timeclock.} This mode is for keeping track of time intervals. You can use it for whatever purpose you like, but the typical scenario is to keep track of how much time you spend working on certain projects.
  \item \textbf{Planner/Remember.} Planner mode is an organizer and day planner for Emacs. It helps you keep track of your completed and pending tasks, daily schedule, and notes in plain text files. Planner mode is based on the aforementioned Emacs-Wiki mode.
  \item \textbf{\href{https://cedet.sourceforge.net/ede.shtml}{EDE (Emacs Development Environment).}} EDE provides the gloss that simplifies the learning curve for all the very useful functionality of building and debugging under emacs. In doing so it attempts to emulate a typical IDE (Integrated Development Environment). What this means is that EDE will manage or create your makefiles and other building environment duties so the developer can concentrate on code, and not support files. In doing so, it will be much easier for new programmers to learn and adopt the GNU ways of doing things.
  \item \textbf{\href{https://www.common-lisp.net/project/slime/}{SLIME.}} SLIME is a major mode for programming in Common Lisp. It essentially replaces \textbf{\href{https://sourceforge.net/projects/ilisp/}{ILISP}} mode which is no longer wholly supported. SLIME works with all major variants of Common Lisp.\\~SLIME uses a socket-based communication/RPC interface between Emacs and Lisp. Slime mode is a minor-mode complementing Lisp mode. It includes many commands for interacting with the Common Lisp process, including a a read-eval-print loop and a Common Lisp debugger written in Emacs Lisp. The debugger pops up an Emacs buffer similar to the Emacs/Elisp debugger.
  \item \textbf{CLHS/HyperSpec (Common Lisp HyperSpec).} CLHS and HyperSpec are minor modes used to look up definitions in the ANSI Common Lisp standard (ANSI X3.226-1994) which is \textbf{\href{https://www.lispworks.com/reference/HyperSpec/}{available on the web}}, courtesy of Kent Pitman and Xanalys.
  \item \textbf{\href{https://www.xref-tech.com}{X-Refactory.}} XRef is a cross referencing tool for C and Java. It lets you lookup definitions, uses of variables and functions, and refactor source code in a type-safe way.
  \item \textbf{\href{https://caml.inria.fr/}{Caml and Tuareg mode.}} These are two major modes for programming in (O)Caml. I prefer the former, but many people prefer the latter. It provides a read-eval-print loop, built-in support for compilation, debugging, and more.
  \item \textbf{\href{https://sourceforge.net/projects/preview-latex}{Preview-LaTeX.}} This Elisp/LaTeX package will render your displayed LaTeX equations right into the editing window where they belong. The purpose of preview-latex is to embed LaTeX environments such as display math or figures into the source buffers. By mouse-clicking, you can open the original text. After editing, another click will just run the region in question through LaTeX and redisplay the new results.
  \item \textbf{W3M.} Summary.
  \item \textbf{\href{https://x-symbol.sourceforge.net/}{X-Symbol.}} This file documents X-Symbol, a package providing semi-WYSIWYG for LaTeX, HTML and other ``token languages''. It uses additional fonts and provide input methods to insert their characters into your document.
  \item \textbf{CC-mode.} This is a GNU Emacs mode for editing files containing C, C++, Objective-C, Java, and CORBA IDL code. CC-mode support template insertion, auto-indenting, key shortcuts for often used expressions and blocks and much, much more. Documentation on cc-mode can be found in the info pages of your Emacs process (type control-h then`i').
  \item \textbf{fill-paragraph.} The fill-* functions reformat sections of text, code, etc. to be more readable. I.e. They can automatically reorganize and/or justify your code, text, HTML, etc. to fit your needs. The primary use of fill-paragraph while coding in Java is cleaning up documentation in comments. Most programmers do not like what it does to their source code by default.
  \item \textbf{\href{https://sourceforge.net/projects/oo-browser/}{The OO Browser.}} OOBR, the object-oriented browser, used to be a free piece of software from Bob Weiner. It is/was a very powerful, flexible, multi-language, source code browser (a la the Smalltalk tradition) for Emacs.
  \item \textbf{\href{https://jdee.sunsite.dk/}{JDEE}}\textbf{: The Java Development Environment for Emacs.}: The JDEE is an Emacs Lisp package that provides a highly configurable Emacs wrapper for command-line Java development tools, such as those provided in JavaSoft's JDK. The JDEE provides menu access to a Java compiler, debugger, and API documenter. The Emacs/JDEE combination adds features typically missing from command-line tools, including:
\end{itemize}
\begin{itemize}
  \item syntax coloring
  \item auto indentation
  \item compile error to source links
  \item source-level debugging
  \item source code browsing
\end{itemize}
\begin{itemize}
  \item The JDEE supports both Emacs (Unix and Windows versions) and XEmacs. It is freely available under the GNU public license.\\~Note that much of the functionality of JDEE is simply JDEE using other packages like cc-mode, font-lock-mode, etc. It does pull all of these packages together very well.
  \item \textbf{Tags.} (from XEmacs info documentation node (XEmacs)Tags:) A ``tags table'' is a description of how a multi-file program is broken up into files. It lists the names of the component files and the names and positions of the functions (or other named sub-units) in each file. Grouping the related files makes it possible to search or replace through all the files with one command. Recording the function names and positions makes possible the `M-.' command which finds the definition of a function by looking up which of the files it is in.\\~Briefly, using tags with Java means that your Emacs knows the location and completion of all interesting features (classes, interfaces, fields, methods, etc.) of your project so that you can (a) jump right to the feature definitions, (b) use \textit{completion} (see the next bullet), (c) do regular expression searches and/or replaces on tags (e.g. global replace of a variable), and more. See the documentation on tags in Emacs info for more information on the use of tags.
  \item \textbf{Completion.} When using tags or OOBR, \textit{completion} can be enabled. When enabled, completion will let Emacs complete partially typed names of interesting features like classes, interfaces, methods, etc. No longer do you have to type those 30 character interface names! Emacs does it for you! Do an Emacs apropos search on ``completion'' (control-h `a') for more information. Completion is normally mapped to meta-tab in most modes. (Completion can work even in text mode - it can complete from your local dictionary!)
  \item \textbf{font-lock-mode.} When Font Lock mode is enabled, text is fontified (i.e. put into new fonts, colors, styles, etc. depending upon what you are typing to make the display of information more clear) as you type it. While font locking can make for a more pretty/clear display, it can seriously slow down typing/development for large files and long-lived Emacs sessions. Possible solutions include refining font locking (see turn-on-fast-lock and related functions), Lazy Font Locking (see lazy-shot-mode), caching font lock information (see fast-lock-cache-directories), and more.
  \item \textbf{Jacob - The Java Commando Base.} Jacob is a Java class browser and project manager for Emacs and includes a powerful class wizard. Jacob is a \textit{Java program} and its functionality overlaps with that of JDEE, OOBR, and XEmacs. We find it most useful to use all of these tools in tandem, adjusting to fit personal taste.
\end{itemize}
Our code standard is partially enforced with this \textbf{elisp code} that provides some customizations to CC-mode and more.
\subsubsection{\href{https://www.jmlspecs.org/}{JML}}
The Java Modeling Language (JML) is a behavioral interface specification language and complementary tool that can be used to specify the behavior of Java modules. It combines the approaches of Eiffel and Larch, with some elements of the refinement calculus. We use JML heavily in the development of all of our Java software. In particular, we use \href{https://www.openjml.org/}{OpenJML} (for compilation and extended static checking) and \href{https://github.com/FreeAndFair/JMLUnitNG}{JMLUnitNG} (for unit test generation).
\section{Code Examples}
(DMZ Note: this section also probably needs either a rewrite, or to be eliminated; the code examples are not here at the moment but we can hyperlink them in, or put them inline)
Template code examples are available for the following classifier types. Note that, because you're just going to change them anyway, we elected not to use ``com.kindsoftware'' package names on the samples.
\subsection{Java Examples}
\begin{itemize}
  \item Abstract Class
  \item Normal Class
  \item Exception Class
  \item Interface
\end{itemize}

Also, other code templates are available. The ``CodeTests'' class is used to test our standards for code structure. The ``Javadoc'' class contains a list of all Javadoc tags defined in this document. You can load this up into your editor and cut and paste from it when writing new documentation.
\begin{itemize}
  \item Code Tests class
  \item Javadoc class
\end{itemize}

The Javadoc documentation generated from all of the above classes is also available.
\subsection{Eiffel Examples}
A single class template is available that highlights many of the recommendations made in this code standard.
\end{comment}

\section{Recommendations for Specific Languages}

\input{languages/lando}

\input{languages/clafer}

\input{languages/sysmlv2}

\input{languages/tamarin}

\input{languages/java}

\input{languages/eiffel}

\section{References}
These guidelines are based on example coding standards from several sources including, but not limited to:
\begin{itemize}
  \item The Caltech Computer Science Infospheres Java Coding Standard, from which this document evolved
  \item Doug Lea's \href{https://gee.cs.oswego.edu/dl/html/javaCodingStd.html}{Java Coding Standard}
  \item \href{https://ambysoft.com/essays/javacodingstandards.html}{Scott Ambler's Java Coding Standards}
  \item Watts Humphrey's book \emph{A Discipline for Software Engineering}, Addison-Wesley, 1995
  \item Mark Fussell's Java Development Standards
  \item The Coding Standards Repository (was hosted at Berkeley) for various languages
  \item Coding Standards for C, C++, and Java by Vision 2000 CCS Package and Application Team
  \item Kent Sandvik's Java Coding Style Guidelines
  \item Taligent's Java Cookbook for porting C++ to Java
  \item Naval Postgraduate School Java Style Guide
  \item The Solo Software Engineering home page
  \item Christiaan Balke, Kors Bos, David Candlin, and Steve Fisher's Eiffel Style Guide
\end{itemize}

\end{document}