From f9181595ba85faec29f86dc256ccf3e9490c036f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 21 May 2022 11:48:46 +0200
Subject: [PATCH] (maybe) better symbol for Ptradd
---
tex/heaplang.sty | 2 +-
tex/heaplang.tex | 4 ++++
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/tex/heaplang.sty b/tex/heaplang.sty
index df6afc2ea..50e739113 100644
--- a/tex/heaplang.sty
+++ b/tex/heaplang.sty
@@ -73,7 +73,7 @@
\newcommand{\unfold}{\langkw{unfold}\spac}
\newcommand{\HLOp}{\circledcirc}
-\newcommand{\Ptradd}{\mathop{+_{\langkw{l}}}}
+\newcommand{\Ptradd}{\mathop{+_{\langkw{L}}}}
\newcommand{\TT}{()}
\newcommand*\poison{\text{\Biohazard}}
diff --git a/tex/heaplang.tex b/tex/heaplang.tex
index 0498d8222..5bdf6e9c4 100644
--- a/tex/heaplang.tex
+++ b/tex/heaplang.tex
@@ -66,6 +66,10 @@ We will leave away the disambiguating subscript when it is clear from the contex
All of this lets us define $\ofval$ as simply applying the value injection (the very first syntactic form of $\Expr$), which makes a lot of things in Coq much simpler.
$\toval$ is defined recursively in the obvious way.
+\langkw{Alloc} takes as first argument the number of heap cells to allocate (must be strictly positive), and as second argument the default value to use for these heap cells.
+This lets one allocate arrays.
+$\Ptradd$ implements pointer arithmetic (the left operand must be a pointer, the right operand an integer), which is used to access array elements.
+
For our set of states and observations, we pick
\begin{align*}
\loc \ni \Loc \eqdef{}& \integer \\
--
GitLab