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?
what is the meaning of indicate substitution by priming metavariables
lo.logic;formal methods