Month: August 2007

Posted on

Axioms of Versioning

Obsolete, please see the latest version

Version 1

An attempt to define syntactical and semantical compatiblity of versions in a formal way. Much derives from the writings of David Orchard, especially the parts on syntactical forward and backward compatibility (though my terminology differs).

  1. Let U be a set of (specifications of) software processable languages {L1, L2, … Ln}
    1. This axiomatization does not concern itself with natural language
  2. The extension of a language Lx is a set of conforming document instances ELx = {Dx1, Dx2, … Dxn}
    1. Iff ELx = ELy then Lx and Ly are extensionally equivalent
      • Lx and Ly may still be different: they may define different semantics for the same syntactical construct
    2. Iff ELx ? ELy then Lx is an extensional sublanguage of Ly
    3. Iff ELx ? ELy then Lx is an extensional superlanguage of Ly
    4. D is the set of all possible documents; or the union of all ELx where Lx ? U
  3. For each Lx ? U there is a set of processors Px = {Px1, Px2, … Pxn} which implement Lx
    1. Each Pxy exhibits behaviour as defined in Lx
    2. Processors can produce and consume documents
    3. Each Pxy produces only documents it can consume itself
    4. At consumption, Pxy may accept or reject documents
  4. The behaviour of a processor Pxy of language Lx is a function Bxy
    1. The function Bxy takes as argument a document, and its value is a processor state
      • We assume a single processor state before each function execution, alternatively we could assume a <state, document> tuple as function argument
    2. If for two processors Pxy and Pxz for language Lx for a document d Bxy(d) = Bxz(d) then the two processors behave similar for d
      • Two processor states for language Lx are deemed equivalent if a human with thorough knowledge of language specification Lx considers the states equivalent. Details may vary insofar as the language specification allows it.
      • Processor equivalence is not intended to be formally or computably decidable; though in some cases it could be.
    3. If ?d ( d ? ELx ? Bxy(d) = Bxz(d) ) then Pxy and Pxz are behaviourally equivalent for Lx
      • If two processors behave the same for every document which belongs to a language Lx, the processors are behaviourally equivalent for Lx.
  5. An ideal language specifies all aspects of desired processor behaviour completely and unambiguously; assume all languages in U are ideal
  6. A processor Px is an exemplary processor of a language Lx if it fully implements language specification Lx; assume all processors for all languages in U are exemplary
    1. Because they are (defined to be) exemplary, every two processors for a language Lx are behaviourally equivalent
    2. ELx = { d is a document ? Px accepts d }
    3. The complement of ELx is the set of everything (normally, every document) which is rejected by Px
    4. The make set MLx = { d is a document ? Px can produce d }
  7. A language Lx is syntactically compatible with Ly iff MLx ? ELy and MLy ? ELx
    • Two languages are syntactically compatible if they accept the documents produced by each other.
    1. A language Ln+1 is syntactically backward compatible with Ln iff MLn ? ELn+1 and Ln+1 is a successor of Ln
      • A language change is syntactically backward compatible if a new receiver accepts all documents produced by an older sender.
    2. A language Ln is syntactically forward compatible with Ln+1 iff MLn+1 ? ELn and Ln+1 is a successor of Ln
      • A language change is syntactically forward compatible if an old receiver accepts all documents produced by a new sender.
  8. A document d can be a member of the extension of any number of languages
    1. Px is an (exemplary) processor of Lx, Py is an (exemplary) processor of language Ly
    2. Two langauges Lx and Ly are semantically equivalent iff ELx = ELy ? ?d ( (d ? ELx ) ? Bx(d) = By(d) )
      • If two languages Lx and Ly take the same documents as input, and their exemplary processors behave the same for every document, the languages are semantically equivalent.
      • Two languages can only be compared if their exemplary processors are similar enough to be compared.
      • Not every two languages can be compared.
      • “Semantic” should not be interpreted in the sense of “formal semantics”.
  9. The semantical equivalence set of a document d for Lx = { y ? ELx | Bx(d) = Bx(y) }
    1. Or: SLx,d = { y ? ELx | Bx(d) = Bx(y) }
      • The semantical equivalence set of a document d is the set of documents which make a processor behave the same as d
      • Semantical equivalence occurs for expressions which are semantically equivalent, such as i = i + 1 and i += 1 for C, or different attribute order in XML etc.
    2. d ? SLx,d
    3. Any two semantical equivalence sets of Lx are necessarily disjunct
      • If z ? SLx,e were also z ? SLx,d then every member of SLx,e would be in SLx,d and vice versa and thus SLx,d = SLx,e
  10. A language Ly is a semantical superlanguage of Lx iff ?d ( d ? MLx ? By(d) = Bx(d) )
    1. For all documents produced by Px, Py behaves the same as Px
      • Equivalence in this case should be decided based on Lx; if Ly makes behavioural distinctions which are not mentioned in Lx, behaviour is still the same as far as Lx is concerned
    2. It follows: ?d ( d ? MLx ? ?SLy,d ( SLy,d ? ELy ? ( SLx,d ? MLx ) ? SLy,d ? By(d) = Bx(d) ) )
      • For any document produced by Px, the part of its semantical equivalence set which Px can actually produce, is a subset of the semantical equivalence set of Py for this document
    3. For all d ? ELx ? d ? MLx there may be many equivalence sets in Ly for which By(d) ? Bx(d)
      • In other words: for documents accepted but not produced by Px, Ly may define additional behaviours
    4. Lx is a semantical sublanguage of Ly iff Ly is a semantical superlanguage of Lx
  11. A language Ln+1 is semantically backward compatible with Ln iff Ln+1 is a semantical superlanguage of Ln and Ln+1 is a successor of Ln
    1. An old sender may expect a newer, but semantically backward compatible, receiver to behave as the sender intended
    2. A language Ln is semantically forward compatible with Ln+1 iff Ln+1 is a semantical sublanguage of Ln and Ln+1 is a successor of Ln
    3. Semantic forward compatibility is only possible if a language loses semantics; i.e. it’s processors exhibit less functionality, and produce less diverse documents
    4. A processor cannot understand what it does not know about yet