Struct SeparationLogic 

pub struct SeparationLogic {
    pub heap_assertion: String,
}

Separation logic over a heap model.

Fields

heap_assertion: String

Implementations

impl SeparationLogic

pub fn new(heap_assertion: impl Into<String>) -> Self

pub fn frame_rule(&self) -> String

Describe the Frame Rule: {P}C{Q} ⊢ {PR}C{QR}.

pub fn small_axiom(&self) -> String

Describe the small axiom for allocation: {emp} x:=alloc(n) {x↦0,…,0}.

pub fn bi_abduction(&self) -> String

Describe bi-abduction: find X, Y such that P * X ⊢ Q * Y.