The Computerate Specifying Paradigm
draft-petithuguenin-computerate-specifying-01

The information below is for an old version of the document
Document Type Active Internet-Draft (individual)
Last updated 2019-11-04 (latest revision 2019-10-28)
Stream (None)
Intended RFC status (None)
Formats pdf htmlized bibtex
Stream Stream state (No stream defined)
Consensus Boilerplate Unknown
RFC Editor Note (None)
IESG IESG state I-D Exists
Telechat date
Responsible AD (None)
Send notices to (None)
Network Working Group                                  M. Petit-Huguenin
Internet-Draft                                    Impedance Mismatch LLC
Intended status: Informational                          November 4, 2019
Expires: May 7, 2020

                  The Computerate Specifying Paradigm
             draft-petithuguenin-computerate-specifying-01

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 May 7, 2020.

Copyright Notice

   Copyright (c) 2019 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 May 7, 2020                  [Page 1]
Internet-Draft           Computerate Specifying            November 2019

Table of Contents

   1.  Introduction  . . . . . . . . . . . . . . . . . . . . . . . .   3
   2.  Overview of Operations  . . . . . . . . . . . . . . . . . . .   4
     2.1.  Libraries . . . . . . . . . . . . . . . . . . . . . . . .   6
     2.2.  Retrofitting Specifications . . . . . . . . . . . . . . .   7
     2.3.  Revision of Standards . . . . . . . . . . . . . . . . . .   8
     2.4.  Content of a Computerate Specification  . . . . . . . . .   8
   3.  Syntax  . . . . . . . . . . . . . . . . . . . . . . . . . . .   8
     3.1.  Syntax Examples . . . . . . . . . . . . . . . . . . . . .   9
       3.1.1.  Data Type . . . . . . . . . . . . . . . . . . . . . .   9
       3.1.2.  Serializer  . . . . . . . . . . . . . . . . . . . . .  10
       3.1.3.  Presentation Format . . . . . . . . . . . . . . . . .  10
     3.2.  Formal Syntax Language  . . . . . . . . . . . . . . . . .  10
       3.2.1.  Augmented BNF (ABNF)  . . . . . . . . . . . . . . . .  11
       3.2.2.  Augmented ASCII Diagrams (AAD)  . . . . . . . . . . .  11
       3.2.3.  Mathematical Formulas . . . . . . . . . . . . . . . .  12
       3.2.4.  RELAX NG Format . . . . . . . . . . . . . . . . . . .  13
       3.2.5.  ASN.1 . . . . . . . . . . . . . . . . . . . . . . . .  13
       3.2.6.  TLS Description Language  . . . . . . . . . . . . . .  13
     3.3.  Proofs for Syntax . . . . . . . . . . . . . . . . . . . .  13
       3.3.1.  Isomorphism Between Type and Formal Language  . . . .  13
       3.3.2.  Data Format Conversion  . . . . . . . . . . . . . . .  15
       3.3.3.  Interoperability with Previous Versions . . . . . . .  16
       3.3.4.  Postel's Law  . . . . . . . . . . . . . . . . . . . .  16
   4.  Semantics . . . . . . . . . . . . . . . . . . . . . . . . . .  18
     4.1.  Typed Petri Nets  . . . . . . . . . . . . . . . . . . . .  18
     4.2.  Semantics Examples  . . . . . . . . . . . . . . . . . . .  21
       4.2.1.  Data Type . . . . . . . . . . . . . . . . . . . . . .  21
       4.2.2.  Serializer  . . . . . . . . . . . . . . . . . . . . .  22
       4.2.3.  Presentation Format . . . . . . . . . . . . . . . . .  22
     4.3.  Formal Semantics Language . . . . . . . . . . . . . . . .  22
       4.3.1.  Cosmogol  . . . . . . . . . . . . . . . . . . . . . .  22
     4.4.  Proofs for Semantics  . . . . . . . . . . . . . . . . . .  23
       4.4.1.  Isomorphism . . . . . . . . . . . . . . . . . . . . .  23
       4.4.2.  Postel's Law  . . . . . . . . . . . . . . . . . . . .  23
       4.4.3.  Termination . . . . . . . . . . . . . . . . . . . . .  23
       4.4.4.  Liveness  . . . . . . . . . . . . . . . . . . . . . .  23
       4.4.5.  Verified Code . . . . . . . . . . . . . . . . . . . .  24
   5.  Acknowledgements  . . . . . . . . . . . . . . . . . . . . . .  24
Show full document text