chiark / gitweb /
strategy: traversal wip proofs
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Sun, 27 May 2012 22:04:59 +0000 (23:04 +0100)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Sun, 27 May 2012 22:04:59 +0000 (23:04 +0100)
strategy.tex

index e3ba372..0f03ddb 100644 (file)
@@ -229,7 +229,7 @@ this must complete eventually.
 
 $\qed$
 
-\section{Traversal phase}
+\section{Traversal phase --- algorithm}
 
 (In general, unless stated otherwise below, when we generate a new
 commit $C$ using one of the commit kind algorith, we update
@@ -366,3 +366,12 @@ $\alg{Merge}$ with $L = W, \; R = S$ and any suitable $M$.
 (Tip Source Merge.)
 
 \end{enumerate}
+
+
+\section{Traversal phase --- proofs}
+
+For each operation called for by the traversal algorithms, we prove
+that the commit generation preconditions are met.
+
+\subsection{Tip Base Merge}
+