Object-Z state schema notation

Question

I'm trying to achieve something like the following with LaTeX:

This is what I have so far:

\documentclass{article}

\usepackage[skins]{tcolorbox}

\newtcolorbox{myframe}[2][]{%
  enhanced,colback=white,colframe=black,coltitle=black,
  sharp corners,boxrule=0.4pt,
  fonttitle=\itshape,
  attach boxed title to top left={yshift=-0.4\baselineskip-0.4pt,xshift=2ex},
  boxed title style={tile,size=minimal,left=0.5mm,right=1mm,
    colback=white,before upper=\strut},
  title=#2,#1
}

\begin{document}

\begin{myframe}{Pop}
  \begin{myframe}{Push}
    Some sample text here that's in the box.
  \end{myframe}
\end{myframe}

\end{document}

I've tried referring to other threads like this one but I am having trouble piecing everything together; I'm mostly struggling with the horizontal line between the variable declarations and premises sections as well as the nesting of boxes. What would be the best way to construct this? Thanks!

Answer 1

The package objectz is quite old but seems to work well with a modern LaTeX. I know nothing about this language (notation,...?) so I may be using the wrong semantic markup, but if you know the language then you can correct the environments.

\documentclass{article}
\usepackage{oz}

\begin{document}

\begin{class}{Buffer}
\also
\sres (max,\Init,Join,Leave) \\
\begin{state}
max: \nat \\
items: \seq MSG
\ST
\# items \leq max
\end{state} \\
\begin{init}
items = \emptyseq
\end{init} \\
\begin{sidebyside}
\begin{schema}{Join}
\Delta(items) \\
msg?: MSG
\ST
\# items < max \\
items' = items \cat \lseq msg?\rseq
\end{schema}
\nextside
\begin{schema}{Leave}
\Delta(items) \\
msg!: MSG
\ST
item \neq \emptyseq \\
items = \lseq msg!\rseq \cat items'
\end{schema}
\end{sidebyside}
\end{class}
\end{document}

Answer 2

A possible solution with tcolorbox. As it uses nested boxes, it won't be breakable between pages.

\documentclass{article}
\usepackage[most]{tcolorbox}
\usepackage{amsmath, amssymb}

\newtcolorbox{mybox}[1][]{%
    enhanced,
    size=title,
    fontupper=\itshape, fonttitle=\itshape,
    sharp corners,
    colback=white, colframe=black, coltitle=black,
    boxrule=1pt, rightrule=0pt,
    segmentation code={\draw (segmentation.west)--++(0:.25\textwidth);},
    attach boxed title to top text left={yshift*=-2mm},
    boxed title style={size=fbox, colback=white, frame hidden},
    #1
}
    
\begin{document}
\begin{mybox}[title={Buffer}]
$\upharpoonright$(max, \textsc{Init}, Join, Leave)
\begin{mybox}
max : $\mathbb{N}$\\
$items:seq\ MSG$
\tcblower
\#items $\leqslant$ max
\end{mybox}
\begin{mybox}[title={\textsc{Init}}]
items $=\langle\ \rangle$
\end{mybox}
\begin{mybox}[nobeforeafter, width=.48\textwidth, title={Join}]
$\Delta$(items)\\
msg? : MSG
\tcblower
\#items $<$ max\\
items' = items$\overset{\smallfrown}{ }\langle$ msg? $\rangle$  
\end{mybox}\hfill
\begin{mybox}[nobeforeafter, width=.48\textwidth, title={Leave}]
$\Delta$(items)\\
msg! : MSG
\tcblower
\#items $\ne \langle \rangle$\\
items $= \langle\text{msg!}\rangle\overset{\smallfrown}{ }$items'  
\end{mybox}
\end{mybox}
\end{document}

Update

In case that a brekable solution is necessary, an alternative to nested boxes could be a boxedraster (or boxeditemize).

\documentclass{article}
\usepackage[most]{tcolorbox}
\usepackage{amsmath, amssymb}
\usepackage{lipsum}
\usepackage[textheight=10cm]{geometry}

\tcbset{
    mybox/.style={%
        enhanced,
        size=title,
        fontupper=\itshape, fonttitle=\itshape,
        sharp corners,
        colback=white, colframe=black, coltitle=black,
        boxrule=1pt, rightrule=0pt,
        segmentation code={\draw (segmentation.west)--++(0:.25\textwidth);},
        attach boxed title to top text left={yshift*=-2mm},
        boxed title style={size=fbox, colback=white, frame hidden},
    }
}
    
\begin{document}
\begin{tcboxeditemize}[raster columns=2, raster equal height=rows, mybox]{mybox, breakable, title={Buffer}}
%
\tcbitem[blank, raster multicolumn=2] $\upharpoonright$(max, \textsc{Init}, Join, Leave)
%
\tcbitem[raster multicolumn=2] 
max : $\mathbb{N}$\\
$items:seq\ MSG$
\tcblower
\#items $\leqslant$ max
%
\tcbitem[raster multicolumn=2, title={\textsc{Init}}] items $=\langle\ \rangle$
%
\tcbitem[title={Join}]
$\Delta$(items)\\
msg? : MSG
\tcblower
\#items $<$ max\\
items' = items$\overset{\smallfrown}{ }\langle$ msg? $\rangle$  
%
\tcbitem[title={Leave}]
$\Delta$(items)\\
msg! : MSG
\tcblower
\#items $\ne \langle \rangle$\\
items $= \langle\text{msg!}\rangle\overset{\smallfrown}{ }$items'  
%
\tcbitem[raster multicolumn=2, title={\textsc{Init}}] items $=\langle\ \rangle$
%
\tcbitem[title={Join}]
$\Delta$(items)\\
msg? : MSG
\tcblower
\#items $<$ max\\
items' = items$\overset{\smallfrown}{ }\langle$ msg? $\rangle$  
%
\tcbitem[title={Leave}]
$\Delta$(items)\\
msg! : MSG
\tcblower
\#items $\ne \langle \rangle$\\
items $= \langle\text{msg!}\rangle\overset{\smallfrown}{ }$items' 
%
\tcbitem[raster multicolumn=2, title={\textsc{Init}}] items $=\langle\ \rangle$ 
\end{tcboxeditemize}
\end{document}

Answer 3

This looks like a combination of box drawing characters like │─┌├└ and \obeyspaces:

\documentclass{article}
\usepackage{amsmath,amssymb}
\usepackage{pmboxdraw}
\begin{document}
\obeyspaces\noindent%
┌──\textit{Buffer}──────────────────────────────────────────────────────\\
│   $\upharpoonright$(\textit{max}, \textsc{Init}, \textit{Join, Leave})\\
│  ┌─────────────────────────────────────────────────────\\
│  │  \textit{max :} $\mathbb{N}$\\
│  │  \textit{items :} seq \textit{MSG}\\
│  ├──────────────\\
│  │  \textit{\#items} $\leqslant$ \textit{max}\\
│  └─────────────────────────────────────────────────────\\
│  ┌──\textsc{Init}───────────────────────────────────────────────\\
│  │  \textit{items} $=\langle\ \rangle$\\
│  └─────────────────────────────────────────────────────\\
│  ┌──\textit{Join}───────────────────  ┌──\textit{Leave}───────────────────\\
│  │  $\Delta$(\textit{items})                        \hskip4.7pt│  $\Delta$(\textit{items})\\
│  │  \textit{msg? : MSG}                   \hskip4pt│  \textit{msg! : MSG}\\
│  ├────────                          \hskip4.8pt├────────\\
│  │  \textit{\#items} $<$ \textit{max}                 \hskip2.3pt│  \textit{\#items} $\ne\langle\ \rangle$\\
│  │  $\mathit{items}' = \mathit{items} \overset{\smallfrown}{ }\langle\mathit{msg?}\rangle$      \hskip4pt│  $\mathit{items} = \langle\mathit{msg!}\rangle\overset{\smallfrown}{ }\mathit{items}'$\\
│  └─────────────────────────  └──────────────────────────\\
└─────────────────────────────────────────────────────────────\\
\end{document}

The original is probably made with a package though, to calculate the various indents. I don't know which package that would be unfortunately :)