Whither Programs as Specifications

TL;DR

This paper explores the extension of algebraic specifications from trace properties to hyperproperties, providing a compositional semantics for imperative programs with loops and examining their implications for program correctness and confidentiality.

Contribution

It introduces a hyperproperty-level algebraic framework and proves a compositional semantics for imperative programs with loops, extending traditional trace-based approaches.

Findings

Hyperproperties can be lifted to algebraic structures.

A compositional semantics for programs with loops is developed.

The semantics aligns with standard semantics for subset-closed hyperproperties.

Abstract

Unifying theories distil common features of programming languages and design methods by means of algebraic operators and their laws. Several practical concerns --- e.g., improvement of a program, conformance of code with design, correctness with respect to specified requirements --- are subsumed by the beautiful notion that programs and designs are special forms of specification and their relationships are instances of logical implication between specifications. Mathematical development of this idea has been fruitful but limited to an impoverished notion of specification: trace properties. Some mathematically precise properties of programs, dubbed hyperproperties, refer to traces collectively. For example, confidentiality involves knowledge of possible traces. This article reports on both obvious and surprising results about lifting algebras of programming to hyperproperties, especially in connection with loops, and suggests directions for further research. The technical results are: a compositional semantics, at the hyper level, of imperative programs with loops, and proof that this semantics coincides with the direct image of a standard semantics, for subset closed hyperproperties.

Equations

$$R\subseteq S\text{mbox}iff⟨R⟩⊑⟨S⟩$$

$$R=sglt\text{mbox};⟨R⟩\text{mbox};\ni$$

$$\langle id_{\Sigma}\rangle=id_{\wp\Sigma}\qquad\langle R\mathbin{\mbox{\small{;}}}S\rangle=\langle R\rangle\mathbin{\mbox{\small{;}}}\langle S\rangle\qquad\langle R\mathbin{\mbox{\small$\cup$}}S\rangle=\langle R\rangle\mathbin{\sqcup}\langle S\rangle$$

$$f\text{mbox};h=h\text{mbox};g\Rightarrow h(\mathsf{lfp}f)=\mathsf{lfp}g$$

$$x+2\le x^{\prime }\supseteq x:=x+3\oplus x:=x+5\supseteq x:=x+3$$

$$\forall\sigma,\sigma^{\prime},\tau,\tau^{\prime}\>\mbox{\small$\bullet$}\>\sigma R\sigma^{\prime}\land\tau R\tau^{\prime}\land\sigma\mathring{\sim}\tau\Rightarrow\sigma^{\prime}\mathring{\sim}\tau^{\prime}$$

$$\forall\sigma,\sigma^{\prime},\tau\>\mbox{\small$\bullet$}\>\sigma R\sigma^{\prime}\land\sigma\mathring{\sim}\tau\Rightarrow\exists\tau^{\prime}\>\mbox{\small$\bullet$}\>\tau R\tau^{\prime}\land\sigma^{\prime}\mathring{\sim}\tau^{\prime}$$

$$\mathring{\sim }\text{mbox};R\subseteq R\text{mbox};\mathring{\sim }$$

$$spec\supseteq design\supseteq \dots \supseteq prog$$

$$c::=atm\mid \mathsf{skip}\mid c;c\mid c\oplus c\mid \mathsf{if}b\mathsf{then}c\mathsf{else}c\mid \mathsf{while}b\mathsf{do}c$$

$$\begin{array}[]{lcl}\llbracket\,\mathsf{skip}\,\rrbracket&\;=&id_{\Sigma}\\ \llbracket\,c\,;d\,\rrbracket&=&\llbracket\,c\,\rrbracket\mathbin{\mbox{\small{;}}}\llbracket\,d\,\rrbracket\\ \llbracket\,c\oplus d\,\rrbracket&=&\llbracket\,c\,\rrbracket\mathbin{\mbox{\small$\cup$}}\llbracket\,d\,\rrbracket\\ \llbracket\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\rrbracket&=&\llbracket\,b\,\rrbracket\mathbin{\mbox{\small{;}}}\llbracket\,c\,\rrbracket\>\mathbin{\mbox{\small$\cup$}}\>\llbracket\,\neg b\,\rrbracket\mathbin{\mbox{\small{;}}}\llbracket\,d\,\rrbracket\\ \llbracket\,\mathsf{while}\ {b}\ \mathsf{do}\ {c}\,\rrbracket&=&\mathsf{lfp}\,\mathsf{F}\\ &\lx@intercol\mbox{where }\mathsf{F}:(\Sigma\mathbin{\multimap}\Sigma)\to(\Sigma\mathbin{\multimap}\Sigma)\mbox{ is defined }\hfil\lx@intercol\\ &\lx@intercol\mathsf{F}R=\llbracket\,b\,\rrbracket\mathbin{\mbox{\small{;}}}\llbracket\,c\,\rrbracket\mathbin{\mbox{\small{;}}}R\>\mathbin{\mbox{\small$\cup$}}\>\llbracket\,\neg b\,\rrbracket\hfil\lx@intercol\end{array}$$

$$\forall p\in\wp\Sigma\>\mbox{\small$\bullet$}\>\mathsf{Agrl}\,(p)\Rightarrow\mathsf{Agrl}\,(\langle R\rangle p)$$

$$\mathsf{Agrl}\,(p)\quad\mbox{iff}\quad\forall\sigma,\tau\>\mbox{\small$\bullet$}\>\sigma\in p\land\tau\in p\Rightarrow\sigma\mathring{\sim}\tau$$

$$\begin{array}[]{lcl}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,atm\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}&\;=&\langle\llbracket\,atm\,\rrbracket\rangle\\ \BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\mathsf{skip}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}&=&id_{\wp\Sigma}\\ \BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,;d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}&=&\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\\ \BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\oplus d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}&=&\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\sqcup}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\\ \BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}&=&\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\>\mathbin{\sqcup}\>\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\\ \BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\mathsf{while}\ {b}\ \mathsf{do}\ {c}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}&=&\mathsf{lfp}\,\mathsf{G}\\ &\lx@intercol\mbox{where }\mathsf{G}:(\wp\Sigma\to\wp\Sigma)\to(\wp\Sigma\to\wp\Sigma)\mbox{ is defined }\hfil\lx@intercol\\ &\lx@intercol\mathsf{G}\varphi=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\varphi\mathbin{\sqcup}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\hfil\lx@intercol\end{array}$$

$$\begin{array}[]{rll}&\langle\mathsf{F}R\rangle\\[-2.15277pt] =&&\quad\mbox{ def $\mathsf{F}$ }\\[-2.15277pt] &\langle\llbracket\,b\,\rrbracket\mathbin{\mbox{\small{;}}}\llbracket\,c\,\rrbracket\mathbin{\mbox{\small{;}}}R\mathbin{\mbox{\small$\cup$}}\llbracket\,\neg b\,\rrbracket\rangle\\[-2.15277pt] =&&\quad\mbox{ $\langle-\rangle$ distributes over $\mathbin{\mbox{\small{;}}}$ and $\mathbin{\mbox{\small$\cup$}}$ }\\[-2.15277pt] &\langle\llbracket\,b\,\rrbracket\rangle\mathbin{\mbox{\small{;}}}\langle\llbracket\,c\,\rrbracket\rangle\mathbin{\mbox{\small{;}}}\langle R\rangle\mathbin{\sqcup}\langle\llbracket\,\neg b\,\rrbracket\rangle\\[-2.15277pt] =&&\quad\mbox{ def $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}$ }\\[-2.15277pt] &\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\langle\llbracket\,c\,\rrbracket\rangle\mathbin{\mbox{\small{;}}}\langle R\rangle\mathbin{\sqcup}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\\[-2.15277pt] =&&\quad\mbox{ induction hypothesis }\\[-2.15277pt] &\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\langle R\rangle\mathbin{\sqcup}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\\[-2.15277pt] =&&\quad\mbox{ def $\mathsf{G}$ }\\[-2.15277pt] &\mathsf{G}\langle R\rangle\\[-2.15277pt] \end{array}$$

$$R=sglt\text{mbox};sglt\text{mbox};⟨⟨R⟩⟩\text{mbox};\ni \text{mbox};\ni$$

$$⟨⟨R⟩⟩\mathbb{A}\subseteq \mathbb{A}$$

$$\begin{array}[]{lcl}\llparenthesis\,atm\,\rrparenthesis&\;=&\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,atm\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\\ \llparenthesis\,\mathsf{skip}\,\rrparenthesis&=&id\\ \llparenthesis\,c\,;d\,\rrparenthesis&=&\llparenthesis\,c\,\rrparenthesis\mathbin{\mbox{\small{;}}}\llparenthesis\,d\,\rrparenthesis\\ \llparenthesis\,c\oplus d\,\rrparenthesis&=&\llparenthesis\,c\,\rrparenthesis\mathbin{\ovee}\llparenthesis\,d\,\rrparenthesis\\ \llparenthesis\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\rrparenthesis&=&\llparenthesis\,c\,\rrparenthesis\mathbin{\triangleleft~{}b~{}\triangleright}\llparenthesis\,d\,\rrparenthesis\\ \llparenthesis\,\mathsf{while}\ {b}\ \mathsf{do}\ {c}\,\rrparenthesis&=&\mathsf{lfp}\,\mathsf{H}\\ &\lx@intercol\mbox{where }\mathsf{H}:(\breve{\wp}(\wp\Sigma)\to\breve{\wp}(\wp\Sigma))\to(\breve{\wp}(\wp\Sigma)\to\breve{\wp}(\wp\Sigma))\mbox{ is defined }\hfil\lx@intercol\\ &\lx@intercol\mathsf{H}\Phi=\llparenthesis\,c\,\rrparenthesis\mathbin{\mbox{\small{;}}}\Phi\mathbin{\triangleleft~{}b~{}\triangleright}\llparenthesis\,\mathsf{skip}\,\rrparenthesis\hfil\lx@intercol\end{array}$$

$$\text{llparenthesis}\mathsf{if}b\mathsf{then}c\mathsf{else}d\text{rrparenthesis}=\text{llparenthesis}b\text{rrparenthesis}\text{mbox};\text{llparenthesis}c\text{rrparenthesis}\bigsqcup \text{llparenthesis}\neg b\text{rrparenthesis}\text{mbox};\text{llparenthesis}d\text{rrparenthesis}$$

$$\text{llparenthesis}\mathsf{while}b\mathsf{do}c\text{rrparenthesis}=\mathsf{lfp}\mathsf{K}\text{mbox}where\mathsf{K}\Phi =\text{llparenthesis}b\text{rrparenthesis}\text{mbox};\text{llparenthesis}c\text{rrparenthesis}\text{mbox};\Phi \bigsqcup \text{llparenthesis}\neg b\text{rrparenthesis}$$

$$\mathsf{K}^{i}\Phi=\begin{array}[t]{l}(\llparenthesis\,x<4\,\rrparenthesis\mathbin{\mbox{\small{;}}}\llparenthesis\,x:=x+1\,\rrparenthesis)^{i}\mathbin{\mbox{\small{;}}}\Phi\;\mathbin{\sqcup}\\ (\mathbin{\sqcup}j::0\leq j<i\>\mbox{\small$\bullet$}\>(\llparenthesis\,x<4\,\rrparenthesis\mathbin{\mbox{\small{;}}}\llparenthesis\,x:=x+1\,\rrparenthesis)^{j}\mathbin{\mbox{\small{;}}}\llparenthesis\,\neg x<4\,\rrparenthesis)\end{array}$$

$$\begin{array}[]{l}\mathbb{Q}_{0}=\{\emptyset\}\\ \mathbb{Q}_{1}=\{\emptyset\}\mathbin{\mbox{\small$\cup$}}\{\{5\}\}=\{\emptyset,\{5\}\}\\ \mathbb{Q}_{2}=\{\emptyset\}\mathbin{\mbox{\small$\cup$}}\{\emptyset\}\mathbin{\mbox{\small$\cup$}}\{\{5\}\}=\{\emptyset,\{5\}\}\\ \mathbb{Q}_{3}=\{\emptyset\}\mathbin{\mbox{\small$\cup$}}\{\emptyset\}\mathbin{\mbox{\small$\cup$}}\{\{4\}\}\mathbin{\mbox{\small$\cup$}}\{\{5\}\}=\{\emptyset,\{4\},\{5\}\}\end{array}$$

$$\text{BeginAccSupp}method=hex,unicode,ActualText=2983\text{f}\text{j}\text{EndAccSupp}\mathsf{while}x<4\mathsf{do}x:=x+1\text{BeginAccSupp}method=hex,unicode,ActualText=2984\text{j}\text{g}\text{EndAccSupp}\{2,5\}=\{4,5\}$$

$$(\Phi\mathbin{\ovee}\Psi)\mathbb{Q}=\{r\mathbin{\mbox{\small$\cup$}}s\mid\exists p\in\mathbb{Q}\>\mbox{\small$\bullet$}\>r\in\Phi(\wp{\,p})\land s\in\Psi(\wp{\,p})\}$$

$$(\Phi\mathbin{\triangleleft~{}b~{}\triangleright}\Psi)\mathbb{Q}=\{r\mathbin{\mbox{\small$\cup$}}s\mid\exists p\in\mathbb{Q}\>\mbox{\small$\bullet$}\>r\in\Phi(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}p))\land s\in\Psi(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}p))\}$$

$$⟨\phi \bigsqcup \psi ⟩⊑⟨\phi ⟩\text{ovee}⟨\psi ⟩$$

$$r\mathbin{\mbox{\small$\cup$}}s\in(\Phi\mathbin{\triangleleft~{}b~{}\triangleright}\Psi)\mathbb{Q}\quad\mbox{ iff }\quad\exists q\in\mathbb{Q}\>\mbox{\small$\bullet$}\>r\in\Phi(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q))\land s\in\Psi(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q))$$

$$\begin{array}[]{rll}&\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\\[-2.15277pt] =&&\quad\mbox{ semantics }\\[-2.15277pt] &\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\sqcup}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\\[-2.15277pt] \sqsubseteq&&\quad\mbox{ by (\ref{eq:joinijoin}) }\\[-2.15277pt] &\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\mathbin{\ovee}\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\\[-2.15277pt] =&&\quad\mbox{ distribute $\langle-\rangle$ over $\mathbin{\mbox{\small{;}}}$, semantics }\\[-2.15277pt] &\llparenthesis\,b\,\rrparenthesis\mathbin{\mbox{\small{;}}}\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\mathbin{\ovee}\llparenthesis\,\neg b\,\rrparenthesis\mathbin{\mbox{\small{;}}}\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\\[-2.15277pt] \sqsubseteq&&\quad\mbox{ assumption, monotonicity }\\[-2.15277pt] &\llparenthesis\,b\,\rrparenthesis\mathbin{\mbox{\small{;}}}\llparenthesis\,c\,\rrparenthesis\mathbin{\ovee}\llparenthesis\,\neg b\,\rrparenthesis\mathbin{\mbox{\small{;}}}\llparenthesis\,d\,\rrparenthesis\\[-2.15277pt] =&&\quad\mbox{ semantics, def of $\mathbin{\triangleleft~{}b~{}\triangleright}$ from $\mathbin{\ovee}$ }\\[-2.15277pt] &\llparenthesis\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\rrparenthesis\\[-2.15277pt] \end{array}$$

$$\begin{array}[]{rll}&\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\varphi\mathbin{\sqcup}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\psi\rangle\mathbb{Q}\\[-2.15277pt] =&&\quad\mbox{ }\\[-2.15277pt] &\{r\mathbin{\mbox{\small$\cup$}}s\mid\exists q\in\mathbb{Q}\>\mbox{\small$\bullet$}\>r=\varphi(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q)\land s=\psi(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q)\}\hskip 30.00005pt(*)\\[-2.15277pt] \end{array}$$

$$\begin{array}[]{rll}&(\langle\varphi\rangle\mathbin{\triangleleft~{}b~{}\triangleright}\langle\psi\rangle)\mathbb{Q}\\[-2.15277pt] =&&\quad\mbox{ }\\[-2.15277pt] &\{r\mathbin{\mbox{\small$\cup$}}s\mid\exists q\in\mathbb{Q}\>\mbox{\small$\bullet$}\>r\in\langle\varphi\rangle(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q))\land s\in\langle\psi\rangle(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q))\}\\[-2.15277pt] =&&\quad\mbox{ }\\[-2.15277pt] &\{r\mathbin{\mbox{\small$\cup$}}s\mid\exists q\in\mathbb{Q}\>\mbox{\small$\bullet$}\>\exists t,u\>\mbox{\small$\bullet$}\>t\subseteq\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q\land u\subseteq\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q\land r=\varphi t\land s=\psi u\}\hskip 30.00005pt(\dagger)\\[-2.15277pt] \end{array}$$

Full text

1 Introduction

A book has proper spelling provided that each of its sentences does. For a book to be captivating and suspenseful — that is not a property that can be reduced to a property of its individual sentences. Indeed, few interesting properties of a book are simply a property of all its sentences. By contrast, many interesting requirements of a program can be specified as so-called trace properties: there is some property of traces (i.e., observable behaviors) which must be satisfied by all the program’s traces.

The unruly mess of contemporary programming languages, design tools, and approaches to formal specification has been given a scientific basis through unifying theories that abstract commonalities by means of algebraic operators and laws. Algebra abstracts from computational notions like partiality and nondeterminacy by means of operators that are interpreted as total functions and which enable equational reasoning. Several practical concerns — such as improving a program’s resource usage while not altering its observable behavior, checking conformance of code with design architecture, checking satisfaction of requirements, and equivalence of two differently presented designs — are subsumed by the beautiful notion that programs and designs111This paper was written with the UTP [19] community in mind, but our use of the term “design” is informal and does not refer to the technical notion in UTP. are just kinds of specification and their relationships are instances of logical implication between specifications. Transitivity of implication yields the primary relationship: the traces of a program are included in the traces allowed by its specification. The mathematical development of this idea has been very successful — for trace properties.

Not all requirements are trace properties. A program should be easy to read, consistent with dictates of style, and amenable to revision for adapting to changed requirements. Some though not all such requirements may be addressed by mathematics; e.g., parametric polymorphism is a form of modularity that facilitates revision through reuse. In this paper we are concerned with requirements that are extensional in the sense that they pertain directly to observable behavior. For a simple example, consider a program acting on variables $hi,lo$ where the initial value of $hi$ is meant to be a secret, on which the final value of $lo$ must not depend. Consider this simple notion of program behavior: a state assigns values to variables, and a trace is a pair: the initial and final states. The requirement cannot be specified as a trace property, but it can be specified as follows: for any two traces $(\sigma,\sigma^{\prime})$ and $(\tau,\tau^{\prime})$, if the initial states $\sigma$ and $\tau$ have the same value for $lo$ then so do the final states. In symbols: $\sigma(lo)=\tau(lo)\Rightarrow\sigma^{\prime}(lo)=\tau^{\prime}(lo)$.

Some requirements involve more than two traces, e.g., “the average response time is under a millisecond” can be made precise by averaging the response time of each trace, over all traces, perhaps weighted by a distribution that represents likelihood of different requests. For a non-quantitative example, consider the requirement that a process in a distributed system should know which process is the leader: something is known in a given execution if it is true in all possible traces that are consistent with what the process can observe of the given execution (such as a subset of the network messages). In the security literature, some information flow properties are defined by closure conditions on the program’s traces, such as: for any two traces, there exists a trace with the high (confidential) events of the first and the low (public) events of the second.

This paper explores the notion that just as a property of books is a set of books, not necessarily defined simply in terms of their sentences, so too a property of programs is a set of programs, not merely a set of traces. The goal is to investigate how the algebra of programming can be adapted for reasoning about non-trace properties. To this end, we focus on the most rudimentary notion of trace, i.e., pre/post pairs, and rudimentary program constructs. We conjecture that the phenomena and ideas are relevant to a range of models, perhaps even the rich notions of trace abstracted by variations on concurrent Kleene algebra [20].

It is unfortunate that the importance of trace properties in programming has led to well established use of the term “property” for trace property, and recent escalation in terminology to “hyperproperty” to designate the general notion of program property — sets of programs rather than sets of traces [10, 9]. Some distinction is needed, so for clarity and succinctness we follow the crowd. The technical contribution of this paper can now be described as follows: we give a lifting of the fixpoint semantics of loops to the “hyper level”, and show anomalies that occur with other liftings. This enables reasoning at the hyper level with usual fixpoint laws for loops, while retaining consistency with standard relational semantics. Rather than working directly with sets of trace sets, our lifting uses a simpler model, sets of state sets; this serves to illustrate the issues and make connections with other models that may be familiar. The conceptual contribution of the paper is to call attention to the challenge of unifying theories of programming that encompass requirements beyond trace properties.

Outline.

Section 2 describes a relational semantics of imperative programs and defines an example program property that is not a trace property. Relational semantics is connected, in Section 3, with semantics mapping sets to sets, like forward predicate transformers. Section 4 considers semantics mapping sets of sets to the same, this being the level at which hyperproperties are formulated. Anomalies with obvious definitions motivate a more nuanced semantics of loops. The main technical result of the paper is Theorem 4.1 in this section, connecting the semantics of Section 4 with that of Section 3. Section 5 connects the preceding results with the intrinsic notion of satisfaction for hyperproperties, and sketches challenges in realizing the dream of reasoning about hyperproperties using only refinement chains. The semantics and theorem are new, but similar to results in prior work discussed in Section 6. Section 7 concludes.

2 Programs and specifications as binary relations

Preliminaries.

We review some standard notions, to fix notation and set the stage. Throughout the paper we assume $\Sigma$ is a nonempty set, which stands for the set of program states, or data values, on which programs act. For any sets $A$, $B$, let $A\mathbin{\multimap}B$ denote the binary relations from $A$ to $B$; that is, $A\mathbin{\multimap}B$ is $\wp(A\times B)$ where $\wp$ means powerset. Unless otherwise mentioned, we consider powersets, including $\Sigma\mathbin{\multimap}\Sigma$, to be ordered by inclusion ($\subseteq$).

We write $A\to B$ for the set of functions from $A$ to $B$. For composition of relations, and in particular composition of functions, we use infix symbol $\mathbin{\mbox{\small{;}}}$ in the forward direction. Thus for relations $R,S$ and elements $x,y$ we have $x(R\mathbin{\mbox{\small{;}}}S)y$ iff \exists z\>\mbox{\small\bullet}\>xRz\land zSy. For a function $f:A\to B$ and element $x\in A$ we write application as $fx$ and let it associate to the left. Composition with $g:B\to C$ is written $f\mathbin{\mbox{\small{;}}}g$, as functions are treated as special relations, so $(f\mathbin{\mbox{\small{;}}}g)x=g(fx)$. The symbol $\mathbin{\mbox{\small{;}}}$ binds tighter than \mathbin{\mbox{\small\cup}} and other operators.

For a relation $R:A\mathbin{\multimap}B$, the direct image $\langle R\rangle$ is a total function $\wp A\to\wp B$ defined by $y\in\langle R\rangle p$ iff \exists x\in p\>\mbox{\small\bullet}\>xRy. It faithfully reflects ordering of relations:

[TABLE]

where $\sqsubseteq$ means pointwise order (i.e., $\varphi\sqsubseteq\psi$ iff \forall p\in\wp A\>\mbox{\small\bullet}\>\varphi\,p\subseteq\psi\,p). We write $\mathbin{\sqcup}$ for pointwise union, defined by (\varphi\mathbin{\sqcup}\psi)\,p=\varphi\,p\mathbin{\mbox{\small\cup}}\psi\,p. The $\sqsubseteq$-least element is the function \lambda p\>\mbox{\small\bullet}\>\emptyset, abbreviated as $\bot$. A relation can be recovered from its direct image:

[TABLE]

where $sglt:A\to\wp A$ maps element $a$ to singleton set $\{a\}$ and $\mathord{\ni}:\wp A\mathbin{\multimap}A$ is the converse of the membership relation. Note that $\bot$ is the direct image of the empty relation. Direct image is functorial and distributes over union:

[TABLE]

We write $id$ for identity function on the set indicated. In fact $\langle-\rangle$ distributes over arbitrary union, i.e., sends any union of relations to the pointwise join of their images. Also, $\langle R\rangle$ is universally disjunctive, and (1) forms a bijection between universally disjunctive functions $\wp A\to\wp B$ and relations $A\mathbin{\multimap}B$.

In this paper we use the term transformer for monotonic functions of type $\wp A\to\wp B$. For $\varphi:\wp A\to\wp B$ to be monotonic is equivalent to $(\mathord{\supseteq}\mathbin{\mbox{\small{;}}}\varphi)\subseteq(\varphi\mathbin{\mbox{\small{;}}}\mathord{\supseteq})$.

We write $\mathsf{lfp}\,$ for the least-fixpoint operator. For monotonic functions $f:A\to A$ and $g:B\to B$ where $A,B$ are sufficiently complete posets that $\mathsf{lfp}\,f$ and $\mathsf{lfp}\,g$ exist, the fixpoint fusion rule says that for strict and continuous $h:A\to B$,

[TABLE]

Inequational forms, such as $f\mathbin{\mbox{\small{;}}}h\leq h\mathbin{\mbox{\small{;}}}g\Rightarrow h(\mathsf{lfp}\,f)\leq\mathsf{lfp}\,g$, are also important.222Fusion rules, also called fixpoint transfer, can be found in many sources, e.g., [1, 4]. We need the form in Theorem 3 of [12], for Kleene approximation of fixpoints.

Relational semantics.

The relational model suffices for reasoning about terminating executions. If we write $x+2\leq x^{\prime}$ to specify a program that increases $x$ by at least two, we can write this simple refinement chain:

[TABLE]

to express that the nondeterministic choice ($\oplus$) between adding 3 or adding 5 refines the specification and is refined in turn by the first alternative. Relations model a good range of operations including relational converse and intersection which are not implementable in general but are useful for expressing specifications. Their algebraic laws facilitate reasoning. For example, choice is modeled as union, so the second step is from a law of set theory: R\mathbin{\mbox{\small\cup}}S\supseteq R.

Equations and inequations may serve as specifications. For example, to express that relation $R$ is deterministic we can write $R^{\cup}\mathbin{\mbox{\small{;}}}R\subseteq id$, where $R^{\cup}$ is the converse of $R$. Note that this uses two occurrences of $R$. Returning to the example in the introduction, suppose $R$ relates states with variables $hi,lo$. To formulate the noninterference property that the final value of $lo$ is independent of the initial value of $hi$, it is convenient to define a relation on states that says they have the same value for $lo$: define $\mathring{\sim}$ by $\sigma\mathring{\sim}\tau$ iff $\sigma(lo)=\tau(lo)$. The property is

[TABLE]

This is a form of determinacy. A weaker notion allows multiple outcomes for $lo$ but the set of possibilities should be independent from the initial value of $hi$.

[TABLE]

This is known as possibilistic noninterference. It can be expressed without quantifiers, by the usual simulation inequality:

[TABLE]

Another equivalent form is $\mathring{\sim}\mathbin{\mbox{\small{;}}}R\mathbin{\mbox{\small{;}}}\mathring{\sim}\;=\;R\mathbin{\mbox{\small{;}}}\mathring{\sim}$, which again uses two occurrences of $R$. The algebraic formulations are attractive, but recall the beautiful idea of correctness proof as a chain of refinements

[TABLE]

This requires the specification to itself be a term in the algebra, rather than an (in)equation between terms.

Before proceeding to investigate this issue, we recall the well known fact that possibilistic noninterference is not closed under refinement of trace sets [21]. Consider $hi,lo$ ranging over bits, so we can write pairs compactly, and consider the set of traces $\{(00,00),\underline{(00,01)},(01,00),\underline{(01,01)},\underline{(10,10)},(10,11),\underline{(11,10)},(11,11)\}$ It satisfies possibilistic noninterference, but if we remove the underlined pairs the result does not; in fact the result copies $hi$ to $lo$.

In the rest of this paper, we focus on deterministic noninterference, $\mathsf{NI}$ for short. It has been advocated as a good notion for security [35] and it serves our purposes as an example.

A signature and its relational model.

To investigate how $\mathsf{NI}$ and other non-trace properties may be expressed and used in refinement chains, it is convenient to focus on a specific signature, the simple imperative language over given atoms (ranged over by $atm$) and boolean expressions (ranged over by $b$).

[TABLE]

For expository purposes we refrain from decomposing the conditional and iteration constructs in terms of choice ($\oplus$) and assertions. That decomposition would be preferred in a more thorough investigation of algebraic laws, and it is evident in the semantic definitions to follow.

Assume that for each $atm$ is given a relation $\llbracket\,atm\,\rrbracket:\Sigma\mathbin{\multimap}\Sigma$, and for each boolean expression $b$ is given a coreflexive relation $\llbracket\,b\,\rrbracket:\Sigma\mathbin{\multimap}\Sigma$. That is, $\llbracket\,b\,\rrbracket$ is a subset of the identity relation $id_{\Sigma}$ on $\Sigma$. For non-atom commands $c$ the relational semantics $\llbracket\,c\,\rrbracket$ is defined in Fig. 1. The fixpoint for loops333 It is well known that loops are expressible in terms of recursion: $\mathsf{while}\ {b}\ \mathsf{do}\ {c}$ can be expressed as \mu X.(b;c;X\mathbin{\mbox{\small\cup}}\neg b) and this is the form we use in semantics. A well known law is \mu X.(b;c;X\mathbin{\mbox{\small\cup}}\neg b)=\mu X.(b;c;X\mathbin{\mbox{\small\cup}}\mathsf{skip});\neg b which factors out the termination condition. is in $\Sigma\mathbin{\multimap}\Sigma$, ordered by $\subseteq$ with least element $\emptyset$.

The language goes beyond ordinary programs, in the sense that atoms are allowed to be unboundedly nondeterministic. They are also allowed to be partial; coreflexive atoms serve as assume and assert statements. Other ingredients are needed for a full calculus of specifications, but here our aim is to sketch ideas that merit elaboration in a more comprehensive theory.

3 Programs as forward predicate transformers

Here is yet another way to specify $\mathsf{NI}$ for a relation $R$:

[TABLE]

where $\mathsf{Agrl}\,$ says that all elements of $p$ agree on $lo$:

[TABLE]

As with the preceding (in)equational formulations, like (3), this is not directly applicable as the specification in a refinement chain, but it does hint that escalating to sets of states may be helpful. Note that $R$ occurs just once in the condition.

Weakest-precondition predicate transformers are a good model for programming algebra: Monotonic functions $\wp\Sigma\to\wp\Sigma$ can model total correctness specifications with both angelic and demonic nondeterminacy. In this paper we use transformers to model programs in the forward direction.

For boolean expression $b$ we define $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}=\langle\llbracket\,b\,\rrbracket\rangle$ so that $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}$ is a filter: $x$ is in $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}p$ iff $x\in p$ and $b$ is true of $x$. The transformer semantics is in Fig. 2. For loops, the fixpoint is for the aforementioned $\bot$ and $\sqsubseteq$.

Linking transformer with relational.

The transformer model may support a richer range of operators than the relational one, but for several reasons it is important to establish their mutual consistency on a common set of operators [18, 19]. A relation can be recovered from its direct image, see (1), so the following is a strong link.

Proposition 1

For all $c$ in the signature, $\langle\llbracket\,c\,\rrbracket\rangle=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}$.

Proof

By induction on $c$.

• •

$\mathsf{skip}$: $\langle\llbracket\,\mathsf{skip}\,\rrbracket\rangle=\langle id_{\Sigma}\rangle=id_{\wp\Sigma\to\wp\Sigma}=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\mathsf{skip}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}$ by definitions and $\langle-\rangle$ law.

• •

$atm$: $\langle\llbracket\,atm\,\rrbracket\rangle=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,atm\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}$ by definition.

• •

$c;d$: $\langle\llbracket\,c;d\,\rrbracket\rangle=\langle\llbracket\,c\,\rrbracket\mathbin{\mbox{\small{;}}}\llbracket\,d\,\rrbracket\rangle=\langle\llbracket\,c\,\rrbracket\rangle\mathbin{\mbox{\small{;}}}\langle\llbracket\,d\,\rrbracket\rangle=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c;d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}$ by definitions, $\langle-\rangle$ laws, and induction hypothesis.

• •

$c\oplus d$: \langle\llbracket\,c\oplus d\,\rrbracket\rangle=\langle\llbracket\,c\,\rrbracket\mathbin{\mbox{\small\cup}}\llbracket\,d\,\rrbracket\rangle=\langle\llbracket\,c\,\rrbracket\rangle\mathbin{\sqcup}\langle\llbracket\,d\,\rrbracket\rangle=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\sqcup}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\oplus d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{} by definitions, $\langle-\rangle$ laws, and induction hypothesis.

• •

$\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}$: \langle\llbracket\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\rrbracket\rangle=\langle\llbracket\,b\,\rrbracket\mathbin{\mbox{\small{;}}}\llbracket\,c\,\rrbracket\mathbin{\mbox{\small\cup}}\llbracket\,\neg b\,\rrbracket\mathbin{\mbox{\small{;}}}\llbracket\,d\,\rrbracket\rangle=\langle\llbracket\,b\,\rrbracket\rangle\mathbin{\mbox{\small{;}}}\langle\llbracket\,c\,\rrbracket\rangle\mathbin{\sqcup}\langle\llbracket\,\neg b\,\rrbracket\rangle\mathbin{\mbox{\small{;}}}\langle\llbracket\,d\,\rrbracket\rangle=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\langle\llbracket\,c\,\rrbracket\rangle\mathbin{\sqcup}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\langle\llbracket\,d\,\rrbracket\rangle=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\sqcup}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{} by definitions, $\langle-\rangle$ laws, and induction hypothesis.

• •

$\mathsf{while}\ {b}\ \mathsf{do}\ {c}$: To prove $\langle\llbracket\,\mathsf{while}\ {b}\ \mathsf{do}\ {c}\,\rrbracket\rangle=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\mathsf{while}\ {b}\ \mathsf{do}\ {c}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}$, unfold the definitions to $\langle\mathsf{lfp}\,\mathsf{F}\rangle=\mathsf{lfp}\,\mathsf{G}$, where $\mathsf{F},\mathsf{G}$ are defined in Figs 1 and 2. This follows by fixpoint fusion, taking $h$ in (2) to be $\langle-\rangle$ so the antecedent to be proved is \forall R\>\mbox{\small\bullet}\>\langle\mathsf{F}R\rangle=\mathsf{G}\langle R\rangle. Observe for any $R$:

[TABLE]

∎

Subsets of $\wp\Sigma\to\wp\Sigma$, such as transformers satisfying Dijkstra’s healthiness conditions, validate stronger laws than the full set of (monotonic) transformers. Healthiness conditions can be expressed by inequations, such as the determinacy inequation $R^{\cup}\mathbin{\mbox{\small{;}}}R\subseteq id$, and used as antecedents in algebraic laws. Care must be taken with joins: not all subsets are closed under pointwise union. Pointwise union does provide joins in the set of all transformers and also in the set of all universally disjunctive transformers.

In addition to transformers as weakest preconditions [4], another similar model is multirelations which are attractive in maintaining a pre-to-post direction [25]. These are all limited to trace properties, though, so we proceed in a different direction.

4 Programs as h-transformers

Given $R:A\mathbin{\multimap}B$, the image $\langle R\rangle$ is a function and functions are relations, so the direct image can be taken: $\langle\langle R\rangle\rangle:\wp^{2}A\to\wp^{2}B$ where $\wp^{2}A$ abbreviates $\wp(\wp A)$. In this paper, monotonic functions of this type are called h-transformers, in a nod to hyper terminology.

The underlying relation can be recovered by two applications of (1):

[TABLE]

More to the point, a quantifier-free formulation of $\mathsf{NI}$ is now in reach. Recall that we have $R\in\mathsf{NI}$ iff \forall p\in\wp\Sigma\>\mbox{\small\bullet}\>\mathsf{Agrl}\,(p)\Rightarrow\mathsf{Agrl}\,(\langle R\rangle p). This is equivalent to

[TABLE]

where the set of sets $\mathbb{A}$ is defined by $\mathbb{A}=\{p\mid\mathsf{Agrl}\,(p)\}$. This is one motivation to investigate $\wp^{2}\Sigma\to\wp^{2}\Sigma$ as a model, rather than $\wp(\Sigma\mathbin{\multimap}\Sigma)$ which is the obvious way to embody the idea that a program is a trace set and a property is a set of programs.

In the following we continue to write $\mathbin{\sqcup}$ and $\sqsubseteq$ for the pointwise join and pointwise order on $\wp^{2}\Sigma\to\wp^{2}\Sigma$. Please note the order is defined in terms of set inclusion at the outer layer of sets and is independent of the order on $\wp\Sigma$. Define $\underline{\bot}=\langle\bot\rangle$ and note that $\underline{\bot}\emptyset=\emptyset$ and $\underline{\bot}\mathbb{Q}=\{\emptyset\}$ for $\mathbb{Q}\neq\emptyset$.

Surprises.

For semantics using h-transformers, some obvious guesses work fine but others do not. The semantics in Fig. 3 uses operators $\mathbin{\ovee}$, $\mathbin{\triangleleft~{}b~{}\triangleright}$ and $\breve{\wp}$ which will be explained in due course. For boolean expressions we simply lift by direct image, defining $\llparenthesis\,b\,\rrparenthesis=\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle$. The same for command atoms, so the semantics of $atm$ is derived from the given $\llbracket\,atm\,\rrbracket$.

The analog of Proposition 1 is that for all $c$ in the signature, $\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle=\llparenthesis\,c\,\rrparenthesis$, allowing laws valid in relational semantics to be lifted to h-transformers. Considering some cases suggests that this could be proved by induction on $c$:

• •

$\mathsf{skip}$: $\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\mathsf{skip}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle=\langle id_{\wp\Sigma}\rangle=\llparenthesis\,\mathsf{skip}\,\rrparenthesis$ by definitions and using that $\langle-\rangle$ preserves identity.

• •

$atm$: $\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,atm\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle=\llparenthesis\,atm\,\rrparenthesis$ by definition.

• •

$c;d$: $\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\mathbin{\mbox{\small{;}}}d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle=\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle=\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\mathbin{\mbox{\small{;}}}\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle=\llparenthesis\,c\,\rrparenthesis\mathbin{\mbox{\small{;}}}\llparenthesis\,d\,\rrparenthesis=\llparenthesis\,c;d\,\rrparenthesis$ by definitions, distribution of $\langle-\rangle$ over $\mathbin{\mbox{\small{;}}}$, and putative induction hypothesis.

These calculations suggest we may succeed with this obvious guess:

[TABLE]

The induction hypothesis would give $\llparenthesis\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\rrparenthesis=\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\mathbin{\sqcup}\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle$. On the other hand, $\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle=\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\sqcup}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle$. Unfortunately these are quite different because the joins are at different levels. In general, for $\varphi$ and $\psi$ of type $\wp\Sigma\to\wp\Sigma$ and $\mathbb{Q}\in\wp^{2}\Sigma$ we have \langle\varphi\mathbin{\sqcup}\psi\rangle\mathbb{Q}=\{\varphi\,p\mathbin{\mbox{\small\cup}}\psi\,p\mid p\in\mathbb{Q}\} whereas (\langle\varphi\rangle\mathbin{\sqcup}\langle\psi\rangle)\mathbb{Q}=\{\varphi\,p\mid p\in\mathbb{Q}\}\mathbin{\mbox{\small\cup}}\{\psi\,p\mid p\in\mathbb{Q}\}. Indeed, the same discrepancy would arise if we define $\llparenthesis\,c\oplus d\,\rrparenthesis=\llparenthesis\,c\,\rrparenthesis\mathbin{\sqcup}\llparenthesis\,d\,\rrparenthesis$.

At this point one may investigate notions of “inner join”, but for expository purposes we proceed to consider a putative definition for loops. Following the pattern for relational and transformer semantics, an obvious guess is

[TABLE]

Consider this program: $\mathsf{while}\ {x<4}\ \mathsf{do}\ {x:=x+1}$. We can safely assume $\llparenthesis\,x<4\,\rrparenthesis$ is $\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,x<4\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle$ and $\llparenthesis\,x:=x+1\,\rrparenthesis$ is $\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,x:=x+1\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle$. As there is a single variable, we can represent a state by its value, for example $\{2,5\}$ is a set of two states. Let us work out $\llparenthesis\,\mathsf{while}\ {x<4}\ \mathsf{do}\ {x:=x+1}\,\rrparenthesis\{\{2,5\}\}$. Now $\llparenthesis\,\mathsf{while}\ {x<4}\ \mathsf{do}\ {x:=x+1}\,\rrparenthesis$ is the limit of the chain $\mathsf{K}^{i}\underline{\bot}$ where $\mathsf{K}^{i}$ means $i$ applications of $\mathsf{K}$. Note that for any $\Phi$ and $i>0$,

[TABLE]

Writing $\mathbb{Q}_{i}$ for $\mathsf{K}^{i}\underline{\bot}\{\{2,5\}\}$ one can derive

[TABLE]

at which point the sequence remains fixed. As in the case of conditional (6), the result is not consistent with the underlying semantics:

[TABLE]

The result should be $\{\{4,5\}\}$ if we are to have the analog of Proposition 1.

A plausible inner join is $\otimes$ defined by (\Phi\otimes\Psi)\mathbb{Q}=\{r\mathbin{\mbox{\small\cup}}s\mid\exists q\in\mathbb{Q}\>\mbox{\small\bullet}\>r\in\Phi\{q\}\land s\in\Psi\{q\}\}. This can be used to define a semantics of $\oplus$ as well as semantics of conditional and loop; the resulting constructs are $\sqsubseteq$-monotonic and enjoy other nice properties.

Indeed, using $\otimes$ in place of $\mathbin{\sqcup}$ in (7), we get $\mathsf{K}^{3}\underline{\bot}\{\{2,5\}\}=\{\{4,5\}\}$, which is exactly the lift of the transformer semantics. There is one serious problem: $\mathsf{K}$ fails to be increasing. In particular, $\underline{\bot}\not\sqsubseteq\mathsf{K}\underline{\bot}$; for example $\underline{\bot}\{\{2,5\}\}=\{\emptyset\}$ but $\mathsf{H}\underline{\bot}\{\{2,5\}\}=\{\{5\}\}$. While this semantics merits further study, we leave it aside because we aim to use fixpoint fusion results that rely on Kleene approximation: This requires $\underline{\bot}\sqsubseteq\mathsf{K}\underline{\bot}$ in order to have an ascending chain, and the use of $\underline{\bot}$ so that $\langle-\rangle$ is strict.

A viable solution.

Replacing singleton by powerset in the definition of $\otimes$, for any h-transformers $\Phi,\Psi:\wp^{2}\Sigma\to\wp^{2}\Sigma$ we define the inner join $\mathbin{\ovee}$ by

[TABLE]

For semantics of conditionals, it is convenient to define, for boolean expression $b$, this operator on h-transformers: $\Phi\mathbin{\triangleleft~{}b~{}\triangleright}\Psi=\llparenthesis\,b\,\rrparenthesis\mathbin{\mbox{\small{;}}}\Phi\mathbin{\ovee}\llparenthesis\,\neg b\,\rrparenthesis\mathbin{\mbox{\small{;}}}\Psi$. It satisfies

[TABLE]

because $\llparenthesis\,b\,\rrparenthesis(\wp\,p)=\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle(\wp\,p)=\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}p)$). These operators are used in Fig. 3 for semantics of conditional and loop.

It is straightforward to prove $\mathbin{\ovee}$ is monotonic: $\Phi\sqsubseteq\Phi^{\prime}$ and $\Psi\sqsubseteq\Psi^{\prime}$ imply $\Phi\mathbin{\ovee}\Psi\sqsubseteq\Phi^{\prime}\mathbin{\ovee}\Psi^{\prime}$. It is also straightforward to prove

[TABLE]

but in general equality does not hold, so we focus on $\mathbin{\triangleleft~{}{\!-\!}~{}\triangleright}$.

Lemma 1

For any $b$, $\mathbin{\triangleleft~{}b~{}\triangleright}$ is monotonic: $\Phi\sqsubseteq\Phi^{\prime}$ and $\Psi\sqsubseteq\Psi^{\prime}$ imply $\Phi\mathbin{\triangleleft~{}b~{}\triangleright}\Psi\sqsubseteq\Phi^{\prime}\mathbin{\triangleleft~{}b~{}\triangleright}\Psi^{\prime}$.

Proof

Keep in mind this is $\sqsubseteq$ at the outer level: $\Phi\sqsubseteq\Phi^{\prime}$ means \forall\mathbb{Q}\>\mbox{\small\bullet}\>\Phi\mathbb{Q}\subseteq\Phi^{\prime}\mathbb{Q} (more sets, not bigger sets, if you will). This follows by monotonicity of $\mathbin{\ovee}$, or using characterization (8) we have

[TABLE]

which implies \exists q\in\mathbb{Q}\>\mbox{\small\bullet}\>r\in\Phi^{\prime}(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q))\land s\in\Psi^{\prime}(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q)) by $\Phi\sqsubseteq\Phi^{\prime}$ and $\Psi\sqsubseteq\Psi^{\prime}$. ∎

With $\llparenthesis\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\rrparenthesis$ defined as in Fig. 3 we have the following refinement.

Lemma 2

$\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\sqsubseteq\llparenthesis\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\rrparenthesis$* provided that $\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\sqsubseteq\llparenthesis\,c\,\rrparenthesis$ and $\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,d\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\sqsubseteq\llparenthesis\,d\,\rrparenthesis$.*

Proof

[TABLE]

∎

This result suggests that we might be able to prove $\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\sqsubseteq\llparenthesis\,c\,\rrparenthesis$ for all $c$, but that would be a weak link between the transformer and h-transformer semantics. A stronger link can be forged as follows.

We say $\mathbb{Q}\in\wp^{2}\Sigma$ is subset closed iff $\mathbb{Q}=\mathsf{ssc}\,\mathbb{Q}$ where the subset closure operator $\mathsf{ssc}\,$ is defined by $p\in\mathsf{ssc}\,\mathbb{Q}$ iff \exists q\in\mathbb{Q}\>\mbox{\small\bullet}\>p\subseteq q. For example, the set $\mathbb{A}$ used in (5) is subset closed. Observe that $\mathsf{ssc}\,=\langle\mathord{\supseteq}\rangle$.

Lemma 3

For transformers $\varphi,\psi:\wp\Sigma\to\wp\Sigma$ and condition $b$, if $\mathbb{Q}=\mathsf{ssc}\,\mathbb{Q}$ then $\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\varphi\mathbin{\sqcup}\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\mathbin{\mbox{\small{;}}}\psi\rangle\mathbb{Q}\;=\;(\langle\varphi\rangle\mathbin{\triangleleft~{}b~{}\triangleright}\langle\psi\rangle)\mathbb{Q}$.

Proof

For the LHS, by definitions:

[TABLE]

For the RHS, again by definitions:

[TABLE]

Now $(*)\subseteq(\dagger)$ by instantiating $t:=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q$ and $u:=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q$, so LHS $\subseteq$ RHS is proved—as expected, given (9). If $\mathbb{Q}$ is subset closed, we get $(\dagger)\subseteq(*)$ as follows. Given $q,t,u$ in $(\dagger)$, let q^{\prime}:=t\mathbin{\mbox{\small\cup}}u. Then $t=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q^{\prime}$ and $u=\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}q$ because $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}$ and $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}$ are filters. And $q^{\prime}\in\mathbb{Q}$ by subset closure. Taking $q:=q^{\prime}$ in $(*)$ completes the proof of RHS $\subseteq$ LHS. ∎

Preservation of subset closure.

In light of Lemma 3, we aim to restrict attention to h-transformers on subset closed sets. To this end we introduce a few notations. The subset-closed powerset operator $\breve{\wp}$ is defined on powersets $\wp A$, by

[TABLE]

To restrict attention to h-transformers of type $\breve{\wp}(\wp\Sigma)\to\breve{\wp}(\wp\Sigma)$ we must show that subset closure is preserved by the semantic constructs.

For any transformer $\varphi$, define $\mathsf{PSC}\,\varphi$ iff $(\mathord{\supseteq}\mathbin{\mbox{\small{;}}}\varphi)=(\varphi\mathbin{\mbox{\small{;}}}\mathord{\supseteq})$. The acronym is explained by the lemma to follow. By definitions, the inclusion $(\mathord{\supseteq}\mathbin{\mbox{\small{;}}}\varphi)\supseteq(\varphi\mathbin{\mbox{\small{;}}}\mathord{\supseteq})$ is equivalent to

[TABLE]

Recall from Section 2 that the reverse, $(\mathord{\supseteq}\mathbin{\mbox{\small{;}}}\varphi)\subseteq(\varphi\mathbin{\mbox{\small{;}}}\mathord{\supseteq})$, is monotonicity of $\varphi$.

Lemma 4

$\mathsf{PSC}\,\varphi$* implies $\langle\varphi\rangle$ preserves subset closure.*

Proof

For any subset closed $\mathbb{Q}$, $\langle\varphi\rangle\mathbb{Q}$ is subset closed because $\langle\mathord{\supseteq}\rangle(\langle\varphi\rangle\mathbb{Q})=\langle\varphi\mathbin{\mbox{\small{;}}}\mathord{\supseteq}\rangle\mathbb{Q}=\langle\mathord{\supseteq}\mathbin{\mbox{\small{;}}}\varphi\rangle\mathbb{Q}=\langle\varphi\rangle(\langle\mathord{\supseteq}\rangle\mathbb{Q})=\langle\varphi\rangle\mathbb{Q}$ using functoriality of $\langle-\rangle$, $\mathsf{PSC}\,\varphi$, and $\mathsf{ssc}\,\mathbb{Q}=\mathbb{Q}$. ∎

It is straightforward to show $\mathsf{PSC}\,\bot$. The following is a key fact, but also a disappointment that leads us away from nondeterminacy.

Lemma 5

If $R$ is a partial function (i.e., $R^{\cup}\mathbin{\mbox{\small{;}}}R\subseteq id$) then $\mathsf{PSC}\,\langle R\rangle$.

Proof

In accord with (11) we show for any $q,r$ that r\subseteq\langle R\rangle q\Rightarrow\exists s\subseteq q\>\mbox{\small\bullet}\>\varphi s=r. Suppose $r\subseteq\langle R\rangle q$. Let s=(\langle R^{\cup}\rangle r)\mathbin{\mbox{\small\cap}}q, so for any $x$ we have $x\in s$ iff $x\in q$ and \exists y\in r\>\mbox{\small\bullet}\>xRy. We have $s\subseteq q$ and it remains to show $\langle R\rangle s=r$, which holds because for any $y$

[TABLE]

Using dots to show domain and range elements, the diagram on the left is an example $R$ such that $\mathsf{PSC}\,\langle R\rangle$ but $R$ is not a partial function. The diagram on the right is a relation, the image of which does not satisfy $\mathsf{PSC}\,$.

{{\bullet}}$${{\bullet}}$${{\bullet}}$${{\bullet}}$${{\bullet}}$${{\bullet}}

{{\bullet}}$${{\bullet}}$${{\bullet}}$${{\bullet}}$${{\bullet}}$${{\bullet}}

As a consequence of Lemmas 4 and 5 we have the following.

Lemma 6

If $R$ is a partial function then $\langle\langle R\rangle\rangle:\wp^{2}{A}\to\wp^{2}{B}$ preserves subset closure.

The theorem.

To prove $\llparenthesis\,c\,\rrparenthesis=\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle$, we want to identify a subset of $\wp\Sigma\to\wp\Sigma$ satisfying two criteria. First, $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,{\!-\!}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}$ can be defined within it, so in particular it is closed under $\mathsf{G}$ in Figure 2. Second, on the subset, $\langle-\rangle$ is strict and continuous into $\breve{\wp}(\wp\Sigma)\to\breve{\wp}(\wp\Sigma)$, to enable the use of fixpoint fusion. Strictness is the reason444In [10], other reasons are given for using $\{\emptyset\}$ rather than $\emptyset$ as the false hyperproperty. to disallow the empty set in (10); it makes $\underline{\bot}$ (which equals $\langle\bot\rangle$) the least element, whereas otherwise the least element would be \lambda\mathbb{Q}\>\mbox{\small\bullet}\>\emptyset. We need the subset to be closed under pointwise union, at least for chains, so that $\langle-\rangle$ is continuous.

Given that $\langle R\rangle$ is universally disjunctive for any $R$, Proposition 1 suggests restricting to universally disjunctive transformers. Lemma 4 suggests restricting to transformers satisfying $\mathsf{PSC}\,$. But we were not able to show the universally disjunctive transformers satisfying $\mathsf{PSC}\,$ are closed under limits. We proceed as follows.

Define $\mathsf{Dom}\,\varphi=\{x\mid\varphi\{x\}\neq\emptyset\}$ and note that $\mathsf{Dom}\langle R\rangle=\mathsf{dom}R$ where $\mathsf{dom}R$ is the usual domain of a relation. By a straightforward proof we have:

Lemma 7

For universally disjunctive $\varphi$ and any $r$ we have \varphi\,r=\varphi(r\mathbin{\mbox{\small\cap}}\mathsf{Dom}\,\varphi).

Lemma 8

For universally disjunctive $\varphi,\psi$ with \mathsf{Dom}\,\varphi\mathbin{\mbox{\small\cap}}\mathsf{Dom}\,\psi=\emptyset, if $\mathsf{PSC}\,\varphi$ and $\mathsf{PSC}\,\psi$ then $\mathsf{PSC}\,(\varphi\mathbin{\sqcup}\psi)$.

Proof

For any $q,r$ with $r\subseteq(\varphi\mathbin{\sqcup}\psi)q$ we need to show \exists s\subseteq q\>\mbox{\small\bullet}\>(\varphi\mathbin{\sqcup}\psi)s=r. First observe

[TABLE]

We use $(*)$ to show that t\mathbin{\mbox{\small\cup}}t^{\prime} witnesses $\mathsf{PSC}\,(\varphi\mathbin{\sqcup}\psi)$, as follows: (\varphi\mathbin{\sqcup}\psi)(t\mathbin{\mbox{\small\cup}}t^{\prime})=\varphi(t\mathbin{\mbox{\small\cup}}t^{\prime})\mathbin{\mbox{\small\cup}}\psi(t\mathbin{\mbox{\small\cup}}t^{\prime})=\varphi t\mathbin{\mbox{\small\cup}}\psi t^{\prime}=s\mathbin{\mbox{\small\cup}}s^{\prime}=r using also the definition of $\mathbin{\sqcup}$, and \varphi(t\mathbin{\mbox{\small\cup}}t^{\prime})=\varphi\,t and \psi(t\mathbin{\mbox{\small\cup}}t^{\prime})=\psi\,t^{\prime} from Lemma 7 and $(*)$. ∎

Lemma 9

If $\Phi$ and $\Psi$ preserve subset closure then $(\Phi\mathbin{\triangleleft~{}b~{}\triangleright}\Psi)\mathbb{Q}$ is subset closed (regardless of whether $\mathbb{Q}$ is).

Proof

Suppose $q$ is in $(\Phi\mathbin{\triangleleft~{}b~{}\triangleright}\Psi)\mathbb{Q}$ and $q^{\prime}\subseteq q$. So according to (8) there are $r,s,p$ with $p\in\mathbb{Q}$, q=r\mathbin{\mbox{\small\cup}}s, $r\in\Phi(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}p))$, and $s\in\Psi(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}p))$. Let r^{\prime}=r\mathbin{\mbox{\small\cap}}q^{\prime} and s^{\prime}=s\mathbin{\mbox{\small\cap}}q^{\prime}, so $r^{\prime}\subseteq r$ and $s^{\prime}\subseteq s$. Because powersets are subset closed, $\Phi(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}p))$ and $\Psi(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}p))$ are subset closed, hence $r^{\prime}\in\Phi(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}p))$ and $s^{\prime}\in\Psi(\wp(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\neg b\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}p))$. As q^{\prime}=r^{\prime}\mathbin{\mbox{\small\cup}}s^{\prime}, we have $q^{\prime}\in(\Phi\mathbin{\triangleleft~{}b~{}\triangleright}\Psi)\mathbb{Q}$. ∎

It is straightforward to prove that $\Phi\mathbin{\ovee}\Psi$ preserves subset closure if $\Phi,\Psi$ do, similar to the proof of Lemma 9. By contrast, $\Phi\otimes\Psi$ does not preserve subset closure even if $\Phi$ and $\Psi$ do.

Next, we confirm that $\llparenthesis\,{\!-\!}\,\rrparenthesis$ can be defined within the monotonic functions $\breve{\wp}(\wp\Sigma)\to\breve{\wp}(\wp\Sigma)$.

Lemma 10

For all $c,\mathbb{Q}$, if $\mathbb{Q}$ is subset closed then so is $\llparenthesis\,c\,\rrparenthesis\mathbb{Q}$, provided that $\mathsf{PSC}\,\langle\llbracket\,atm\,\rrbracket\rangle$ for every $atm$.

Proof

By induction on $c$.

• •

$atm$: $\llparenthesis\,atm\,\rrparenthesis$ is $\langle\langle\llbracket\,atm\,\rrbracket\rangle\rangle$ so by assumption $\mathsf{PSC}\,\langle\llbracket\,atm\,\rrbracket\rangle$ and Lemma 4.

• •

$\mathsf{skip}$: immediate.

• •

$c;d$: by definitions and induction hypothesis.

• •

$c\oplus d$: by induction hypothesis and observation above about $\mathbin{\ovee}$.

• •

$\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}$: by Lemma 9 and induction hypothesis.

• •

$\mathsf{while}\ {b}\ \mathsf{do}\ {c}$: Because $\underline{\bot}$ is least in $\breve{\wp}(\wp\Sigma)\to\breve{\wp}(\wp\Sigma)$, we have $\underline{\bot}\sqsubseteq\mathsf{H}\underline{\bot}$, so using monotonicity of $\mathsf{H}$ we have Kleene iterates. Suppose $\mathbb{Q}$ is subset closed. To show $\mathsf{lfp}\,\mathsf{H}\,\mathbb{Q}$ is subset closed, note that $\mathsf{lfp}\,\mathsf{H}=\mathsf{H}^{\gamma}\,\mathbb{Q}$ where $\gamma$ is some ordinal. We show that $\mathsf{H}^{\alpha}\,\mathbb{Q}$ is subset closed, for every $\alpha$ up to $\gamma$, by ordinal induction.

• –

$\mathsf{H}^{0}\,\mathbb{Q}=\mathbb{Q}$ which is subset closed.

• –

$\mathsf{H}^{\alpha+1}\,\mathbb{Q}=(\llparenthesis\,c\,\rrparenthesis\mathbin{\mbox{\small{;}}}\mathsf{H}^{\alpha}\mathbin{\triangleleft~{}b~{}\triangleright}\llparenthesis\,\mathsf{skip}\,\rrparenthesis)\mathbb{Q}$ by definition of $\mathsf{H}$. Now $\mathsf{H}^{\alpha}$ preserves subset closure by the ordinal induction hypothesis, and $\llparenthesis\,c\,\rrparenthesis$ preserves subset closure by the main induction hypothesis. So $\llparenthesis\,c\,\rrparenthesis\mathbin{\mbox{\small{;}}}\mathsf{H}^{\alpha}$ preserves subset closure, as does $\llparenthesis\,\mathsf{skip}\,\rrparenthesis$. Hence $\llparenthesis\,c\,\rrparenthesis\mathbin{\mbox{\small{;}}}\mathsf{H}^{\alpha}\mathbin{\triangleleft~{}b~{}\triangleright}\llparenthesis\,\mathsf{skip}\,\rrparenthesis$ preserves subset closure by Lemma 9.

• –

$\mathsf{H}^{\beta}\,\mathbb{Q}=(\mathbin{\sqcup}_{\alpha<\beta}H^{\alpha})\mathbb{Q}$ (for non-0 limit ordinal $\beta$), which in turn equals \mathbin{\mbox{\small\cup}}_{\alpha<\beta}(H^{\alpha}\,\mathbb{Q}) because $\mathbin{\sqcup}$ is pointwise. By induction, each $H^{\alpha}\,\mathbb{Q}$ is subset closed, and closure is preserved by union, so we are done. ∎

Returning to the two criteria for a subset of $\wp\Sigma\to\wp\Sigma$, suppose $\llbracket\,atm\,\rrbracket$ is a partial function, for all $atm$ — in short, atoms are deterministic. If in addition $c$ is $\oplus$-free, then $\llbracket\,c\,\rrbracket$ is a partial function. Under these conditions, by Proposition 1, $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}$ is the direct image of a partial function.

Let $\mathsf{IPF}$ be the subset of $\wp\Sigma\to\wp\Sigma$ that are direct images of partial functions, i.e., \mathsf{IPF}=\{\varphi\in\wp\Sigma\to\wp\Sigma\mid\exists R\>\mbox{\small\bullet}\>\varphi=\langle R\rangle\mbox{ and }R^{\cup}\mathbin{\mbox{\small{;}}}R\subseteq id\}. Observe that $\mathsf{IPF}$ is closed under $\mathsf{G}$, because for $\varphi\in\mathsf{IPF}$ with $\varphi=\langle R\rangle$ we have \mathsf{G}\langle R\rangle=\langle\llbracket\,b\,\rrbracket\rangle\mathbin{\mbox{\small{;}}}\langle\llbracket\,c\,\rrbracket\rangle\mathbin{\mbox{\small{;}}}\langle R\rangle\mathbin{\sqcup}\langle\llbracket\,\neg b\,\rrbracket\rangle=\langle\llbracket\,b\,\rrbracket\mathbin{\mbox{\small{;}}}\llbracket\,c\,\rrbracket\mathbin{\mbox{\small{;}}}R\rangle\mathbin{\sqcup}\langle\llbracket\,\neg b\,\rrbracket\rangle=\langle\llbracket\,b\,\rrbracket\mathbin{\mbox{\small{;}}}\llbracket\,c\,\rrbracket\mathbin{\mbox{\small{;}}}R\mathbin{\mbox{\small\cup}}\llbracket\,\neg b\,\rrbracket\rangle and the union is of partial functions with disjoint domains so it is a partial function. We have $\bot\sqsubseteq\mathsf{G}\bot$ because $\bot$ is the least element in $\wp\Sigma\to\wp\Sigma$. By Lemma 6, when $\langle-\rangle$ is restricted to $\mathsf{IPF}$, its range is included in $\breve{\wp}(\wp\Sigma)\to\breve{\wp}(\wp\Sigma)$. In $\mathsf{IPF}$, lubs of chains are given by pointwise union, so $\langle-\rangle$ is a strict and continuous function from $\mathsf{IPF}$ to $\breve{\wp}(\wp\Sigma)\to\breve{\wp}(\wp\Sigma)$.

To state the theorem, we write $\dot{=}$ for extensional equality on h-transformers of type $\breve{\wp}(\wp\Sigma)\to\breve{\wp}(\wp\Sigma)$, i.e., equal results on all subset closed $\mathbb{Q}$.

Theorem 4.1

$\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle\;\dot{=}\;\llparenthesis\,c\,\rrparenthesis$, provided atoms are deterministic and $c$ is $\oplus$-free.

Proof

By induction on $c$. For the cases of $\mathsf{skip}$, atoms, and $\mathbin{\mbox{\small{;}}}$ the arguments preceding (6) are still valid. For conditional, observe

[TABLE]

Finally, the loop:

[TABLE]

The antecedent for fusion is \forall\varphi\>\mbox{\small\bullet}\>\langle\mathsf{G}\varphi\rangle=\mathsf{H}\langle\varphi\rangle and it holds because for any $\varphi$:

[TABLE]

5 Specifications and refinement

We wish to conceive of specifications as miraculous programs that can achieve by refusing to do, can choose the best angelically, and can compute the uncomputable. We wish to establish rigorous connections between programs and specifications, perhaps by deriving a program that can be automatically compiled for execution, perhaps by deriving a specification that can be inspected to determine the usefulness or trustworthiness of the program. A good theory may enable automatic derivation in one direction or the other, but should also account for ad hoc construction of proofs. Simple reasons should be expressed simply, so algebraic laws and transitive refinement chains are important. In this inconclusive section, we return to the general notion of hyperproperty and consider how the h-transformer semantics sheds light on refinement for hyperproperties. Initially we leave aside the signature/semantics notations.

Let $R:\Sigma\mathbin{\multimap}\Sigma$ be considered as a program, and $\mathbb{H}$ be a hyperproperty, that is, $\mathbb{H}$ is a set of programs. Formally: $\mathbb{H}\in\wp(\Sigma\mathbin{\multimap}\Sigma)$. For $R$ to satisfy $\mathbb{H}$ means, by definition, that $R\in\mathbb{H}$. The example of possibilistic noninterference shows that in general trace refinement is unsound: $R\in\mathbb{H}$ does not follow from $S\in\mathbb{H}$ and $S\supseteq R$. It does follow in the case that $\mathbb{H}$ is subset closed. Given that $\wp(\Sigma\mathbin{\multimap}\Sigma)$ is a huge space, one may hope that specifications of practice interest may lie in relatively tame subsets. Let us focus on subset closed hyperproperties, for which one form of chain looks like

[TABLE]

Although this is a sound way to prove $R\in\mathbb{H}$, it does not seem sufficient, at least for examples like $\mathsf{NI}$ which require some degree of determinacy. The problem is that for intermediate steps of trace refinement it is helpful to use nondeterminacy for the sake of abstraction and underspecification, so finding suitable $S$ and $T$ may be difficult. One approach to this problem is to use a more nuanced notion of refinement, that preserves a hyperproperty of interest. For confidentiality, Banks and Jacob explore this approach in the setting of UTP [6].

Another form of chain looks like

[TABLE]

where most intermediate terms are at the hyper level, i.e., $\mathbb{S}$ and $\mathbb{T}$ are, like $\mathbb{H}$, elements of $\wp(\Sigma\mathbin{\multimap}\Sigma)$. The chain is a sound way to prove $R\in\mathbb{H}$, even if $\mathbb{H}$ is not subset closed. But in what way are the intermediates $\mathbb{S},\mathbb{T},\ldots$ expressed, and by what reasoning are the containments established? What is the relevant algebra, beyond elementary set theory?

The development in Section 4 is meant to suggest a third form of chain:

[TABLE]

Here the intermediate terms are of type $\breve{\wp}(\wp\Sigma)\to\breve{\wp}(\wp\Sigma)$ and $\sqsubseteq$ is the pointwise ordering (used already in Section 4). The good news is that if the intermediate terms are expressed using program notations, they may be amenable to familiar laws such as those of Kleene algebra with tests [23, 38], for which relations are a standard model. A corollary of Theorem 4.1 is that the laws hold for deterministic terms expressed in the signature (4). To make this claim precise one might spell out the healthiness conditions of elements in the range of $\llparenthesis\,{\!-\!}\,\rrparenthesis$, but more interesting would be to extend the language with specification constructs, using (in)equational conditions like $R^{\cup}\mathbin{\mbox{\small{;}}}R\subseteq id$ as antecedents in conditional laws of healthy fragments. We leave this aside in order to focus on a gap in our story so far.

The third form of chain is displayed with elipses on the left because we lack an account of specifications! Our leading example, $\mathsf{NI}$, is defined as a set of relations, whereas in (14) the displayed chain needs the specification, say $\Psi$, to have type $\breve{\wp}(\wp\Sigma)\to\breve{\wp}(\wp\Sigma)$. The closest we have come is the characterization $R\in\mathsf{NI}$ iff $\langle\langle R\rangle\rangle\mathbb{A}\subseteq\mathbb{A}$, see (5). But this is a set containment, whereas we seek $\Psi$ with $R\in\mathsf{NI}$ iff $\Psi\sqsupseteq\langle\langle R\rangle\rangle$. In the rest of this section we sketch two ways to proceed.

On the face of it, $\Psi\sqsupseteq\langle\langle R\rangle\rangle$ seems problematic because $\sqsupseteq$ is an ordering on functions. Given a particular set $p\in\wp\Sigma$ with $\mathsf{Agrl}\,p$, a noninterfering $R$ makes specific choice of value for $lo$ whereas specification $\Psi$ should allow any value for $lo$ provided that the choice does not depend on the initial value for $hi$. One possibility is to escalate further and allow the specification to be a relation $\breve{\wp}(\wp\Sigma)\mathbin{\multimap}\breve{\wp}(\wp\Sigma)$. To define such a relation, first lift the predicate $\mathsf{Agrl}\,$ on sets to the filter $\widehat{\mathsf{Agrl}\,}:\wp(\wp\Sigma)\mathbin{\multimap}\wp(\wp\Sigma)$ defined by

[TABLE]

Note that $\mathbb{A}=\widehat{\mathsf{Agrl}\,}(\wp\Sigma)$. More to the point, $\widehat{\mathsf{Agrl}\,}\,\mathbb{Q}=\mathbb{Q}$ just if each $p\in\mathbb{Q}$ satisfies $\mathsf{Agrl}\,$. Now define $\mathbf{NI}$, as a relation $\mathbf{NI}:\breve{\wp}(\wp\Sigma)\mathbin{\multimap}\breve{\wp}(\wp\Sigma)$, by

[TABLE]

This achieves the following: $R\in\mathsf{NI}$ iff $\mathbf{NI}\supseteq\langle\langle R\rangle\rangle$. But this inclusion does not compose transitively with $\sqsupseteq$ in the third form of chain, so we proceed no further in this direction.

The second way to proceed can be described using a variation on the h-transformer semantics of Section 4. It will lead us back to the second form of chain, (13), in particular for $\mathsf{NI}$ as $\mathbb{H}$. The idea resembles UTP models of reactive processes [19, Chapt. 8], in which an event history is related to its possible extension. Here we use just pre-post traces, as follows. Let $\mathsf{Trc}=\Sigma\times\Sigma$. Consider a semantics $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,{\!-\!}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\prime}$ such that $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\prime}$ has type $\wp\mathsf{Trc}\to\wp\mathsf{Trc}$. Instead of transforming an initial state to a final one (or rather, state set as in $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,{\!-\!}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}$), an initial trace $(\sigma,\tau)$ is mapped to traces $(\sigma,\upsilon)$ for $\upsilon$ with $\tau\llbracket\,c\,\rrbracket\upsilon$. The semantics $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,{\!-\!}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\prime}$ is not difficult to define (or see [3, sec. 2]). The upshot is that for $S\in\wp\mathsf{Trc}$, the trace set $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\prime}S$ is the relation $S\mathbin{\mbox{\small{;}}}\llbracket\,c\,\rrbracket$. In particular, let $init$ be $id_{\Sigma}$, viewed as an element of $\wp\mathsf{Trc}$. We get $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\prime}init=\llbracket\,c\,\rrbracket$, the relation denoted by $c$. Lifting, we obtain a semantics $\llparenthesis\,{\!-\!}\,\rrparenthesis^{\prime}$, at the level $\wp^{2}\mathsf{Trc}\to\wp^{2}\mathsf{Trc}$, such that $\llparenthesis\,c\,\rrparenthesis^{\prime}\{init\}$ contains $\llbracket\,c\,\rrbracket$. (In light of Theorem 4.1 and the discussion preceding it, we do not expect $\llparenthesis\,c\,\rrparenthesis^{\prime}\{init\}$ to be just the singleton $\{\llbracket\,c\,\rrbracket\}$, as $\{init\}$ is not subset closed.) This suggests a chain of the form $\mathsf{NI}\supseteq\ldots\supseteq\Psi(\mathsf{ssc}\,\{init\})\supseteq\llparenthesis\,c\,\rrparenthesis^{\prime}(\mathsf{ssc}\,\{init\})\,\mathord{\ni}\,\llbracket\,c\,\rrbracket$ which proves that $\llbracket\,c\,\rrbracket$ satisfies $\mathsf{NI}$ — and which may be derived from a subsidiary chain of refinements like $\Psi\sqsupseteq\llparenthesis\,c\,\rrparenthesis^{\prime}$ as in the third form of chain, independent of the argument $\mathsf{ssc}\,\{init\}$.

This approach has been explored in the setting of abstract interpretation, where the intermediate terms are obtained as a computable approximation of a given program’s semantics. To sketch the the idea we first review abstract interpretation for trace properties. Mathematically, abstract interpretation is very close to data refinement, where intermediate steps involve changes of data representation. For example, the state space $\Sigma$ of $R:\Sigma\mathbin{\multimap}\Sigma$ would be connected with another, say $\Delta$, by a coupling relation $\rho:\Delta\mathbin{\multimap}\Sigma$ subject to a simulation condition such as $S\mathbin{\mbox{\small{;}}}\rho\supseteq\rho\mathbin{\mbox{\small{;}}}R$, recall (3). With a functional coupling, the connection could be $\rho(\langle S\rangle\Delta)\sqsupseteq\langle R\rangle(\rho\Delta)$.

Let $T\in\Sigma\mathbin{\multimap}\Sigma$ be a trace set intended as a trace property specification. In terms of the trace-computing semantics $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,{\!-\!}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\prime}$ above, $c$ satisfies $T$ provided that $T\supseteq\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\prime}init$. It can be proved by the following chain, ingredients of which are to be explained.

[TABLE]

Here $\gamma:A\to\wp\mathsf{Trc}$ is like $\rho$ above, mapping some convenient domain $A$ to traces. The element $a\in A$ is supposed to be an approximation of the initial traces, i.e., $\gamma\,a\supseteq init$. Thus the containment $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\prime}(\gamma\,a)\supseteq\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\prime}init$ is by monotonicity of semantics. The next containment, $\gamma(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\sharp}a)\supseteq\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\prime}(\gamma a)$, involves an “abstract” semantics $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\sharp}:A\to A$. Indeed, the containment is the soundness requirement for such semantics. What remains is the containment $T\supseteq\gamma(\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\sharp}\,a)$ which needs to be checked somehow. Typically, $\gamma$ is part of a Galois connection, i.e., it has a lower adjoint $\alpha:\wp\mathsf{Trc}\to A$ and the latter check is equivalent to $\alpha T\geq\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\sharp}\,a$ where $\geq$ is the order on $A$. Ideally it is amenable to automation, but that is beside the point.

The point is to escalate this story to the hyper level, in a chain of this form:

[TABLE]

Now $\gamma$ has type $A\to\wp^{2}\mathsf{Trc}$. Again, the abstract semantics should be sound — condition $\gamma(\llparenthesis\,c\,\rrparenthesis^{\sharp}\,a)\supseteq\llparenthesis\,c\,\rrparenthesis^{\prime}(\gamma\,a)$ — now with respect to a set-of-trace-set semantics $\llparenthesis\,{\!-\!}\,\rrparenthesis^{\prime}$ that corresponds to our Fig. 3. The element $a\in A$ now approximates the set $\mathsf{ssc}\,\{init\}$ and $\llparenthesis\,c\,\rrparenthesis^{\prime}(\gamma\,a)\supseteq\llparenthesis\,c\,\rrparenthesis^{\prime}(\mathsf{ssc}\,\{init\})$ is by monotonicity. The step $\mathbb{H}\supseteq\gamma(\llparenthesis\,c\,\rrparenthesis^{\sharp}\,a)$ may again be checked at the abstract level as $\alpha\mathbb{H}\geq\llparenthesis\,c\,\rrparenthesis^{\sharp}\,a$. Of course $\mathbb{H}$ is a hyperproperty so the goal is to prove the program is an element of $\mathbb{H}$. This follows provided that $\llparenthesis\,c\,\rrparenthesis^{\prime}(\mathsf{ssc}\,\{init\})\;\mathord{\ni}\;\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\prime}init$, a connection like our Theorem 4.1 except for moving from $\wp\Sigma$ to $\wp\mathsf{Trc}$.

6 Related work

The use of algebra in unifying theories of programming has been explored in many works including the book that led to the UTP meetings [19, 37, 20]. Methodologically oriented works include the books by Morgan [28] and by Bird and de Moor [8].

The term hyperproperty was introduced by Clarkson and Schneider who among other things mention that refinement at the level of trace properties is admissible for proving subset closed hyperproperties [10]. They point out that the topological classification of trace properties, i.e., safety and liveness, corresponds to similar notions dubbed hypersafety and hyperliveness. Subset closed hyperproperties strictly subsume hypersafety. As it happens, $\mathsf{NI}$ is in the class called 2-safety that specifies a property as holding for every pair of traces. For fixed $k$, one can encode $k$-safety by a product program, each trace of which represents $k$ traces of the original. Some interesting requirements, such as quantitative information flow, are not in $k$-safety for any $k$.

Epistemic logic is the topic of a textbook [16] and has been explored in the security literature [5]. Mantel considers a range of security properties via closure operators [24]. The limited usefulness of trace refinement for proving $\mathsf{NI}$ even for deterministic programs, as in the chain (12), is discussed by Assaf and Pasqua [3, 27]. The formulation of possibilistic noninterference as $\mathring{\sim}\mathbin{\mbox{\small{;}}}R\mathbin{\mbox{\small{;}}}\mathring{\sim}\;=\;R\mathbin{\mbox{\small{;}}}\mathring{\sim}$ is due to Joshi and Leino [22] and resembles the formulation of Roscoe et al. [35].

The textbook of Back and von Wright [4] explores predicate transformer semantics and refinement calculus. The use of $sglt$ and $\mathord{\ni}$ in (1) is part of the extensive algebra connecting predicate transformers and relations using categorical notions [14]. Upward closed sets of predicates play an important role in that algebra [33], which should be explored in connection with the present investigation and its potential application to higher order programs. The extension of functional programming calculus to imperative refinement is one setting in which strong laws (Cartesian closure) for a well-behaved subset are expressed as implications with inequational antecedents [32, 34]. These works use backward predicate transformers in order to model general specifications and in particular the combination of angelic and demonic nondeterminacy. Alternative models with similar aims can be found in Martin et al [25] and Morris et al [31].

A primary precursor to this paper is the dissertion work of Assaf, which targets refinement chains in the style of abstract interpretation [13, 11]. Assaf’s work [3] introduced a set-of-sets lifted semantics from which our h-transformer semantics is adapted. In keeping with the focus on static analysis, Assaf shows the lifted semantics is an approximation of the underlying one.555Assaf et al use fixpoint fusion in the inequational form mentioned following (2), to prove soundness of the derived abstract semantics. Their inequational result corresponding to our Theorem is proved, in the loop case, using explicit induction on approximation chains. See the proof of Theorem 1 in [3]. Assaf derives an abstraction $\llparenthesis\,c\,\rrparenthesis^{\sharp}$ for dependency from $\llparenthesis\,c\,\rrparenthesis$ (for every $c$), by calculation, following Cousot [11] and similar to data refinement by calculation [17, 30]. For this purpose and others, it is essential that loops be interpreted by fixpoint at the level of sets-of-sets, so standard fixpoint reasoning is applicable, as opposed to using $\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\mathsf{while}\ {b}\ \mathsf{do}\ {c}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle$ which is not a fixed point per se. In fact Assaf derives two abstract semantics $\llparenthesis\,c\,\rrparenthesis^{\sharp}$: one for dependency ($\mathsf{NI}$) and one that computes cardinality of low-variation, for quantitative information flow properties. The cardinality abstraction is not in $k$-safety for any $k$.

Pasqua and Mastroeni have aims similar to Assaf et al, and investigate several variations on set-of-set semantics of loops [27]. Our example in Section 4 is adapted from their work, which uses examples to suggest that Assaf’s definition (called “mixed” in [27]) is preferable. They also point out that, for subset closed hyperproperties, these variations are precise in the sense of our Theorem 4.1, strengthening the inequation in Assaf et al.666Displayed formula $\{\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,c\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}T\mid T\in\mathbb{T}\}\subseteq\llparenthesis\,c\,\rrparenthesis\mathbb{T}$ following Theorem 1 of [3].

A peculiarity of these works is the treatment of conditionals. Assaf et al take the equation $\llparenthesis\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\rrparenthesis=\langle\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}\rangle$ as the definition of $\llparenthesis\,\mathsf{if}\ {b}\ \mathsf{then}\ {c}\ \mathsf{else}\ {d}\,\rrparenthesis$, but this makes the definition of $\llparenthesis\,{\!-\!}\,\rrparenthesis$ non-compositional and thus the inductive proofs a little sketchy. We do not discern an explicit definition in [27], but do find remarks like this: “The definition of the collecting hypersemantics is just the additive lift…for every statement, except for the while case.” As a description of fact, it is true for subset closed hyperproperties (see our Theorem 4.1). But it is unsuitable as a definition. We show that a proper definition is possible.

Non-compositionality for sequence and conditional seems difficult to reconcile with proofs by induction on program structure. It also results in anomalies, e.g., the formulation in Assaf et al means that in case $c$ is a loop, the semantics of $c$ is different from the semantics of $\mathsf{if}\ {true}\ \mathsf{then}\ {c}\ \mathsf{else}\ {\mathsf{skip}}$. The obscurity is rectified when the semantics is restricted to subset closed sets, as spelled out in detail in an unpublished note [15], confirming remarks by Pasqua and Mastroeni [26] elaborated in [27] and in the thesis of Pasqua.

Although similar to results in the preceding work, our results are novel in a couple of ways. Our semantics is for a language with nondeterminacy, unlike theirs. Of course, nondeterministic programs typically fail to satisfy $\mathsf{NI}$ and related properties, and our theorem is restricted to deterministic programs. A minor difference is that they formulate loop semantics in a standard form mentioned in Footnote 3 that asserts the negated guard following the fixpoint rather than as part of it. Those works use semantics mapping traces to traces (or sets of sets thereof), like our $\BeginAccSupp{method=hex,unicode,ActualText=2983}\textnormal{\char 102\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 106\relax}\EndAccSupp{}\,{\!-\!}\,\BeginAccSupp{method=hex,unicode,ActualText=2984}\textnormal{\char 106\relax}\mathchoice{\mkern-4.05mu}{\mkern-4.05mu}{\mkern-4.3mu}{\mkern-4.8mu}\textnormal{\char 103\relax}\EndAccSupp{}^{\prime}$ and $\llparenthesis\,{\!-\!}\,\rrparenthesis^{\prime}$, said to be needed in order to express dependency. We have shown that states-to-states is sufficient to exhibit both the anomaly and its resolution. It suffices for specifications of the form (5) and may facilitate further investigation owing to its similarity to many variations on relational and transformer semantics.

Apropos $\mathsf{NI}$, the formulation (5) is robust in the sense that it generalizes to more nuanced notions of dependency: $\langle\langle R\rangle\rangle\mathbb{P}\subseteq\mathbb{Q}$ where $\mathbb{P}$ expresses agreement on some projections of the input (e.g., agreement on whether a password guess is correct, or agreement on some aggregate value derived from a sensitive database) and $\mathbb{Q}$ expresses agreement on the observable output values. Such policies are the subject of  [36].

Banks and Jacob [6] formalize general confidentiality policies in UTP and introduce a family of confidentiality preserving refinement relations. The ideas are developed further in subsequent work where confidentiality-violating refinements are represented as miracles [7] and knowledge is explicitly represented by sets encoding alternate executions, an idea that has appeared in other guises [29, 2].

7 Conclusion

We have given what, to the best of our knowledge, is the first compositional definition of semantics at the hyper level. Moreover, we proved that it is the lift of a standard semantics when restricted to subset closed hyperproperties. The latter is a “forward collecting semantics” in the terminology of abstract interpretation. The new semantics includes nondeterministic constructs, although the lifting equivalence is only proved for the deterministic fragment.

Although deterministic noninterference is a motivating example, there are other interesting hyperproperties such as quantitative information flow that can be expressed in subset closed form and which are meaningful for nondeterministic programs. This is one motivation for further investigation including the following questions. $\bullet$ Restricting to subset closed hyperproperties is sufficient to make possible a compositional fixpoint semantics at the hyper level that accurately represents the underlying semantics — is it necessary? $\bullet$ The h-transformer semantics allows nondeterministic choice and nondeterministic atoms that satisfy $\mathsf{PSC}\,$ (in light of Lemma 10), and in fact the definitions can be used for a semantics in $\wp(\wp\Sigma)\to\wp(\wp\Sigma)$, into which $\breve{\wp}(\wp\Sigma)\to\breve{\wp}(\wp\Sigma)$ embeds nicely owing to joins being pointwise — but what exactly is the significance of determinacy? $\bullet$ Are disjunctive transformers satisfying $\mathsf{PSC}\,$ closed under join? What is a good characterization of transformers that are images of relations?

A person not familiar with unifying theories of programming may wonder whether programs are specifications. Indeed, the author was once criticized by a famous computer scientist who objected to refinement calculi on the grounds that underspecification and nondeterminacy are distinct notions that ought not be confused — though years later he published a soundness proof for a program logic, in which that confusion is exploited to good effect. A positive answer to the question can be justified by embedding programs in a larger space of specifications, in a way that faithfully reflects a given semantics of programs. Our theorem is a result of this kind. The larger space makes it possible to express important requirements such as noninterference. However, we do not put forward a compelling notion of specification that encompasses hyperproperties and supports a notion of refinement analogous to existing notions for trace properties. Rather, we hope the paper inspires or annoys the reader enough to provoke further research.

Acknowledgements. Anonymous reviewers offered helpful suggestions and pointed out errors, omissions, and infelicities in an earlier version.

The authors were partially supported by NSF award 1718713.