de.uka.ilkd.key.proof.mgt

Class RuleJustificationBySpec

java.lang.Object

de.uka.ilkd.key.proof.mgt.RuleJustificationBySpec

All Implemented Interfaces:

RuleJustification

public class RuleJustificationBySpec
extends java.lang.Object
implements RuleJustification

Field Summary

Fields

Modifier and Type	Field and Description
private Contract	spec

Constructor Summary

Constructors

Constructor and Description
RuleJustificationBySpec(Contract spec)

Method Summary

Modifier and Type	Method and Description
Contract	getSpec()
boolean	isAxiomJustification() Contracts for stubs are considered axioms; other contracts not.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

spec

private final Contract spec

Constructor Detail

RuleJustificationBySpec

public RuleJustificationBySpec(Contract spec)

Method Detail

isAxiomJustification

public boolean isAxiomJustification()

Contracts for stubs are considered axioms; other contracts not.

Specified by:

isAxiomJustification in interface RuleJustification

getSpec

public Contract getSpec()