Enum ConcurrencyLogic 

pub enum ConcurrencyLogic {
    ConcurrentSL,
    Iris,
    VST,
    CompCert,
}

Concurrency logic variants.

Variants

ConcurrentSL

Concurrent Separation Logic (O’Hearn 2007).

Iris

Iris framework (Jung et al., step-indexed, higher-order).

VST

Verified Software Toolchain (VST, CompCert-based).

CompCert

CompCert memory model with separation logic.

Implementations

impl ConcurrencyLogic

pub fn is_machine_checked(&self) -> bool

Returns true if this logic has been machine-checked in a proof assistant.

pub fn uses_separation_logic(&self) -> bool

Returns true if this logic is based on separation logic.

Trait Implementations

impl Clone for ConcurrencyLogic

fn clone(&self) -> ConcurrencyLogic

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ConcurrencyLogic

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for ConcurrencyLogic

fn eq(&self, other: &ConcurrencyLogic) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for ConcurrencyLogic

impl StructuralPartialEq for ConcurrencyLogic