This is a question about the usage of "indicate substitution by priming metavariables". For example, in the separation logic(it is not important whether familiar to this logic), I can understand the allocation rule, i.e., from a state that the memory is empty, and execute the command $v:=cons(\overline{e})$, then the result is the momery is allocated. the rule is as following $$\overline{\{emp\} ~~v:=con(\overline{e})~~\{v\mapsto \overline{e}\}}$$ where $v$ is not free in $\overline{e}$, abbreviate $e_1, ...,e_n$ by $\overline{e}$

Explanation:precondition $emp$,as a assertion, denotes the empty memory. $v:=cons(\overline{e})$ denote allocate the a new block of memory consisting of $n$ cells, the $i$th cell has the content $e_i$ and give the block address to the variable $v$, then the postcondition is that the memory is the block which is referenced by $v$.

The following is where "indicate substitution by priming metavariables" happens.

In the above rule, we indicate substitution by priming metavariables denoting expressions and assertions, e.g., we write $e_i'$ for $e_i/v\to v'$. we also abbreviate $e_1, ...,e_n$ by $\overline{e}$ and $e_1',...,e_n'$ by $\overline{e}'$

the above allocation rule turns to be $$\overline{\{v=v'\land emp\} ~~v:=con(\overline{e}) ~~\{v\mapsto \overline{e}'\}}$$

My question is what's the meaning of "write $e_i'$ for $e_i/v\to v'$"?,

and what the meaning of $v=v'$, $v\mapsto \overline{e}'$ in above rule?

  • $\begingroup$ The question is fairly incomprehensible as is. Can you give a reference where this notation appears? $\endgroup$ – Emil Jeřábek supports Monica Nov 5 '14 at 13:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.