Variables as resource in Hoare logic.
R Bornat, C Calcagno… - 21st Annual IEEE …, 2006 - repository.mdx.ac.uk
R Bornat, C Calcagno, M Parkinson
21st Annual IEEE Symposium on Logic in Computer Science (LICS …, 2006•repository.mdx.ac.ukThis paper contains a model and a proof of soundness for a range of program logics based
on separation logic and including the notions of permission and ownership for stack
variables. It shows that there is no loss of expressive power (all proofs in Hoare logic are
expressible). This permits the construction of program-reasoning tools that use the notion of
'variables as resource'. This is a highly technical piece of work, and its impact will emerge
when more tools have been constructed. Variables-as-resource will be necessary if such …
on separation logic and including the notions of permission and ownership for stack
variables. It shows that there is no loss of expressive power (all proofs in Hoare logic are
expressible). This permits the construction of program-reasoning tools that use the notion of
'variables as resource'. This is a highly technical piece of work, and its impact will emerge
when more tools have been constructed. Variables-as-resource will be necessary if such …
This paper contains a model and a proof of soundness for a range of program logics based on separation logic and including the notions of permission and ownership for stack variables. It shows that there is no loss of expressive power (all proofs in Hoare logic are expressible). This permits the construction of program-reasoning tools that use the notion of ‘variables as resource'. This is a highly technical piece of work, and its impact will emerge when more tools have been constructed. Variables-as-resource will be necessary if such tools are to emerge.
repository.mdx.ac.uk
