Alloy::AlloyVisitor Class Reference

The AlloyVisitor class transforms a class into Alloy compatible code. More...

Inheritance diagram for Alloy::AlloyVisitor:

Static Public Member Functions
static void	init ()
Static Public Member Functions inherited from Model::Visitor< AlloyVisitor, Export::SourceFragment * >
static void	addType (std::function< Export::SourceFragment *(AlloyVisitor *, NodeType *)> f)

Static Private Member Functions
template<typename ListElement >
static Export::SourceFragment *	list (Model::TypedList< ListElement > *aList, AlloyVisitor *v, const QString &fragmentType={})

Static Private Attributes
static QString	currentClass_ = ""
static bool	inContract_ = false
static bool	inFact_ = false

Additional Inherited Members
Public Types inherited from Model::Visitor< AlloyVisitor, Export::SourceFragment * >
using	BaseVisitorType = AlloyVisitor
using	VisitFunctionInstance = std::function< Export::SourceFragment *(AlloyVisitor *, Node *)>
using	VisitorResultType = Export::SourceFragment *
Public Member Functions inherited from Model::Visitor< AlloyVisitor, Export::SourceFragment * >
virtual	~Visitor ()
Export::SourceFragment *	visit (Node *n)
virtual Export::SourceFragment *	visitChildren (Node *n)
Protected Member Functions inherited from Model::Visitor< AlloyVisitor, Export::SourceFragment * >
virtual VisitFunctionInstance	findFunctionForId (int id)

Detailed Description

The AlloyVisitor class transforms a class into Alloy compatible code.

It uses the code contracts specified in a class to generate spefifications of the Alloy models.

Member Function Documentation

init()

void Alloy::AlloyVisitor::init ( )

static

list()

template<typename ListElement >

Export::SourceFragment * Alloy::AlloyVisitor::list ( Model::TypedList< ListElement > *  aList, AlloyVisitor *  v, const QString &  fragmentType = {}  )

staticprivate

Member Data Documentation

currentClass_

QString Alloy::AlloyVisitor::currentClass_ = ""

staticprivate

inContract_

bool Alloy::AlloyVisitor::inContract_ = false

staticprivate

inFact_

bool Alloy::AlloyVisitor::inFact_ = false

staticprivate