@Immutable
public abstract class Tlsf
extends java.lang.Object
Modifier and Type | Class | Description |
---|---|---|
static class |
Tlsf.Semantics |
Constructor | Description |
---|---|
Tlsf() |
Modifier and Type | Method | Description |
---|---|---|
java.util.List<Formula> |
assert_() |
|
Formula |
assume() |
|
protected void |
check() |
|
abstract java.lang.String |
description() |
|
java.util.List<Formula> |
guarantee() |
|
Formula |
initially() |
|
abstract java.util.BitSet |
inputs() |
|
int |
numberOfInputs() |
|
abstract java.util.BitSet |
outputs() |
|
Formula |
preset() |
|
Formula |
require() |
|
abstract Tlsf.Semantics |
semantics() |
|
abstract Tlsf.Semantics |
target() |
|
abstract java.lang.String |
title() |
|
java.util.List<LabelledFormula> |
toAssertGuaranteeConjuncts() |
|
LabelledFormula |
toFormula() |
|
abstract java.util.List<java.lang.String> |
variables() |
@Default public java.util.List<Formula> assert_()
@Default public Formula assume()
public abstract java.lang.String description()
@Default public java.util.List<Formula> guarantee()
@Default public Formula initially()
public abstract java.util.BitSet inputs()
public abstract java.util.BitSet outputs()
public abstract java.util.List<java.lang.String> variables()
@Default public Formula preset()
@Default public Formula require()
public abstract Tlsf.Semantics semantics()
public abstract Tlsf.Semantics target()
public abstract java.lang.String title()
@Derived public int numberOfInputs()
@Derived public LabelledFormula toFormula()
@Derived public java.util.List<LabelledFormula> toAssertGuaranteeConjuncts()
@Check protected void check()