X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=article.tex;h=0c10bcf095b02696681a91a33539695b10371f9a;hp=1781fe5c73edfbb008d8b00c2e15c63661066190;hb=cc2806a584319dd6210fb8a89d342d1110d8dc67;hpb=284c804bd15c5465bb6a1ded29369435f4f699e4 diff --git a/article.tex b/article.tex index 1781fe5..0c10bcf 100644 --- a/article.tex +++ b/article.tex @@ -46,6 +46,14 @@ \newcommand{\py}{\pay{P}} \newcommand{\pn}{\pan{P}} +\newcommand{\pc}{\pa{C}} +\newcommand{\pcy}{\pay{C}} +\newcommand{\pcn}{\pan{C}} + +\newcommand{\pd}{\pa{D}} +\newcommand{\pdy}{\pay{D}} +\newcommand{\pdn}{\pan{D}} + \newcommand{\pl}{\pa{L}} \newcommand{\ply}{\pay{L}} \newcommand{\pln}{\pan{L}} @@ -61,8 +69,8 @@ %\newcommand{\hasparents}{\underaccent{1}{>}} %\newcommand{\hasparents}{{% % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}} -\newcommand{\hasparents}{>_{\mkern-7.0mu _1}} -\newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}} +\newcommand{\hasparents}{>_{\mkern-7.0mu _{1:}}} +\newcommand{\areparents}{<_{\mkern-14.0mu _{1:}\mkern+5.0mu}} \renewcommand{\implies}{\Rightarrow} \renewcommand{\equiv}{\Leftrightarrow} @@ -82,13 +90,39 @@ \newcommand{\patch}{{\mathcal P}} \newcommand{\base}{{\mathcal B}} +\newcommand{\depsreq}{{\mathcal D}} \newcommand{\patchof}[1]{\patch ( #1 ) } \newcommand{\baseof}[1]{\base ( #1 ) } +\newcommand{\depsreqof}[1]{\depsreq ( #1 ) } + +\newcommand{\allpatches}{\Upsilon} +\newcommand{\assign}{\leftarrow} +\newcommand{\iassign}{\leftarrow} +%\newcommand{\assign}{' =} + +\newcommand{\alg}[1]{\text{\bf #1}} +\newcommand{\setmerge}{\alg{merge}} +\newcommand{\setmergeof}[3]{\setmerge\left\langle #1 \;\middle\langle #2 \middle\rangle\; #3 \right\rangle} +%\newcommand{\setmergeof}[3]{\setmerge\left\lgroup #1 \;\middle\lmoustache\; #2 \;\middle\rmoustache\; #3 \right\rgroup} +%\newcommand{\setmergeof}[3]{\setmerge\left\rmoustache #1 \middle\rmoustache #2 \middle\lmoustache #3 \right\lmoustache} +%\newcommand{\setmergeof}[3]{\setmerge\left\lfloor #1 \middle\lfloor #2 \middle\rfloor #3 \right\rfloor} \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} } \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} } +\newcommand{\hasdirdep}{\succ_{\mkern-7.0mu _1}} +\newcommand{\hasdep}{\succ} +\newcommand{\isdep}{\prec} +\newcommand{\isdirdep}{\prec_{\mkern-18.0mu _1}{\mkern+10mu}} + +\newcommand{\tip}{ T } +\newcommand{\tipa}[1]{ \tip^{#1} } +\newcommand{\tipcn}{ \tipa \pcn } +\newcommand{\tipcy}{ \tipa \pcy } +\newcommand{\tipdn}{ \tipa \pdn } +\newcommand{\tipdy}{ \tipa \pdy } + %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}} \newcommand{\bigforall}{% \mathop{\mathchoice% @@ -97,6 +131,13 @@ {\hbox{\normalsize$\forall$}}% {\hbox{\scriptsize$\forall$}}}% } +\newcommand{\bigexists}{% + \mathop{\mathchoice% + {\hbox{\huge$\exists$}}% + {\hbox{\Large$\exists$}}% + {\hbox{\normalsize$\exists$}}% + {\hbox{\scriptsize$\exists$}}}% +} \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}} \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}} @@ -113,6 +154,8 @@ \begin{document} +\chapter{Data model} + \input{notation.tex} \input{invariants.tex} \input{lemmas.tex} @@ -124,4 +167,8 @@ \input{anticommit.tex} \input{merge.tex} +\chapter{Update strategy} + +\input{strategy.tex} + \end{document}