The Computerate Specifying Paradigm
draft-petithuguenin-computerate-specifying-04
Network Working Group M. Petit-Huguenin
Internet-Draft Impedance Mismatch LLC
Intended status: Experimental September 12, 2020
Expires: March 16, 2021
The Computerate Specifying Paradigm
draft-petithuguenin-computerate-specifying-04
Abstract
This document specifies a paradigm named Computerate Specifying,
designed to simultaneously document and formally specify
communication protocols. This paradigm can be applied to any
document produced by any Standard Developing Organization (SDO), but
this document targets specifically documents produced by the IETF.
Status of This Memo
This Internet-Draft is submitted in full conformance with the
provisions of BCP 78 and BCP 79.
Internet-Drafts are working documents of the Internet Engineering
Task Force (IETF). Note that other groups may also distribute
working documents as Internet-Drafts. The list of current Internet-
Drafts is at https://datatracker.ietf.org/drafts/current/.
Internet-Drafts are draft documents valid for a maximum of six months
and may be updated, replaced, or obsoleted by other documents at any
time. It is inappropriate to use Internet-Drafts as reference
material or to cite them other than as "work in progress."
This Internet-Draft will expire on March 16, 2021.
Copyright Notice
Copyright (c) 2020 IETF Trust and the persons identified as the
document authors. All rights reserved.
This document is subject to BCP 78 and the IETF Trust's Legal
Provisions Relating to IETF Documents (https://trustee.ietf.org/
license-info) in effect on the date of publication of this document.
Please review these documents carefully, as they describe your rights
and restrictions with respect to this document. Code Components
extracted from this document must include Simplified BSD License text
as described in Section 4.e of the Trust Legal Provisions and are
provided without warranty as described in the Simplified BSD License.
Petit-Huguenin Expires March 16, 2021 [Page 1]
Internet-Draft Computerate Specifying September 2020
Table of Contents
1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . 4
2. Overview . . . . . . . . . . . . . . . . . . . . . . . . . . 5
3. Terminology . . . . . . . . . . . . . . . . . . . . . . . . . 5
4. Private Specifications . . . . . . . . . . . . . . . . . . . 6
4.1. Private Specifications for New Documents . . . . . . . . 9
4.2. Private Specifications for Existing Documents . . . . . . 10
5. Self-Contained Specifications . . . . . . . . . . . . . . . . 11
5.1. PDU Descriptions . . . . . . . . . . . . . . . . . . . . 11
5.1.1. PDU Examples . . . . . . . . . . . . . . . . . . . . 12
5.1.2. Calculations from PDU . . . . . . . . . . . . . . . . 15
5.1.3. PDU Representations . . . . . . . . . . . . . . . . . 16
5.2. State Machines . . . . . . . . . . . . . . . . . . . . . 17
5.3. Proofs . . . . . . . . . . . . . . . . . . . . . . . . . 18
5.3.1. Wire Type vs Abstract Type . . . . . . . . . . . . . 19
5.3.2. Data Format Conversion . . . . . . . . . . . . . . . 22
5.3.3. Postel's Law . . . . . . . . . . . . . . . . . . . . 22
5.3.4. Implementability . . . . . . . . . . . . . . . . . . 25
5.3.5. Termination . . . . . . . . . . . . . . . . . . . . . 26
5.3.6. Liveness . . . . . . . . . . . . . . . . . . . . . . 26
6. Importing Specifications . . . . . . . . . . . . . . . . . . 26
6.1. Common Modules . . . . . . . . . . . . . . . . . . . . . 28
6.1.1. Generating AsciiDoc . . . . . . . . . . . . . . . . . 28
6.1.2. Common Data Types . . . . . . . . . . . . . . . . . . 29
6.1.3. Calculations . . . . . . . . . . . . . . . . . . . . 33
6.1.4. Typed Petri Nets . . . . . . . . . . . . . . . . . . 34
6.1.5. Representations . . . . . . . . . . . . . . . . . . . 36
6.1.5.1. Bit Diagrams . . . . . . . . . . . . . . . . . . 37
6.1.5.2. Message Sequence Charts . . . . . . . . . . . . . 38
6.2. Packages for Meta-Languages . . . . . . . . . . . . . . . 38
6.2.1. Augmented BNF (ABNF) . . . . . . . . . . . . . . . . 41
6.2.2. Augmented Packet Header Diagrams (APHD) . . . . . . . 42
6.2.3. Cosmogol . . . . . . . . . . . . . . . . . . . . . . 44
6.3. Packages for Protocols . . . . . . . . . . . . . . . . . 44
6.3.1. Type Transformations . . . . . . . . . . . . . . . . 45
6.3.2. Extended Registries . . . . . . . . . . . . . . . . . 48
7. Exporting Specifications . . . . . . . . . . . . . . . . . . 50
7.1. Standard Library . . . . . . . . . . . . . . . . . . . . 50
7.2. Transclusions . . . . . . . . . . . . . . . . . . . . . . 52
Show full document text