A B C D E F G I L M N O P R S T U V W Z

A

addInfix(String, String, int) - Method in class net.sourceforge.czt.z2b.BTermWriter

Add an infix operator to the ops_ table

addPred(Pred, List<Pred>) - Method in class net.sourceforge.czt.z2b.Z2B

Flatten conjuncts and add them to the given list.

addPreds(List<Pred>, List<Pred>) - Method in class net.sourceforge.czt.z2b.Z2B

Apply addPred to a LIST of predicates.

addPrefix(String, String) - Method in class net.sourceforge.czt.z2b.BTermWriter

Add a prefix operator to the ops_ table

AND_PREC - Static variable in class net.sourceforge.czt.z2b.BTermWriter

andPred(Pred, Pred) - Static method in class net.sourceforge.czt.z2b.Create

Create a simple AndPred.

arg - Static variable in class net.sourceforge.czt.z2b.BTermWriter

ASSIGN_PREC - Static variable in class net.sourceforge.czt.z2b.BTermWriter

B

beginPrec(int) - Method in class net.sourceforge.czt.z2b.BWriter

Starts an output region of a given precedence.

beginPrec() - Method in class net.sourceforge.czt.z2b.BWriter

Start a new LOOSEST region without adding any "(".

BException - Exception in net.sourceforge.czt.z2b

This exception is raised when the Z spec cannot be translated into B.

BException(String) - Constructor for exception net.sourceforge.czt.z2b.BException

Constructor for BException

BMachine - Class in net.sourceforge.czt.z2b

This class represents a B abstract machine.

BMachine(String) - Constructor for class net.sourceforge.czt.z2b.BMachine

Constructor for BMachine

bName(ZName) - Static method in class net.sourceforge.czt.z2b.BWriter

Convert a Z Name into a legal B name.

bName(String) - Static method in class net.sourceforge.czt.z2b.BWriter

Convert a string into a legal B name

bOp(String) - Method in class net.sourceforge.czt.z2b.BTermWriter

Get the B operator that corresponds to a Z operator, or null.

BOperation - Class in net.sourceforge.czt.z2b

This class represents a B operation (not initialisation).

BOperation(String, BMachine) - Constructor for class net.sourceforge.czt.z2b.BOperation

Constructor for BOperation

BTermWriter - Class in net.sourceforge.czt.z2b

This class prints a Z predicate/expression out in B syntax.

BTermWriter(BWriter) - Constructor for class net.sourceforge.czt.z2b.BTermWriter

Constructor for BWriteTerm

BWriter - Class in net.sourceforge.czt.z2b

This class extends java.io.PrintWriter with some B-specific print methods.

BWriter(Writer, String) - Constructor for class net.sourceforge.czt.z2b.BWriter

Constructor for BWriter

C

Classifier - Class in net.sourceforge.czt.z2b

Classifier(SectTypeEnvAnn, String) - Constructor for class net.sourceforge.czt.z2b.Classifier

COMMA_PREC - Static variable in class net.sourceforge.czt.z2b.BTermWriter

containsInputs(Term) - Method in class net.sourceforge.czt.z2b.FreeVarChecker

containsPrimesOrOutputs(Term) - Method in class net.sourceforge.czt.z2b.FreeVarChecker

continueSection(String, String) - Method in class net.sourceforge.czt.z2b.BWriter

Start the second/third/...

Create - Class in net.sourceforge.czt.z2b

This class provides a factory for creating Z AST terms.

Create() - Constructor for class net.sourceforge.czt.z2b.Create

createBWriter(URL) - Static method in class net.sourceforge.czt.z2b.Main

Create the output B file.

currSection_ - Variable in class net.sourceforge.czt.z2b.BWriter

D

declareVar(ZName, Expr, List<String>, List<Pred>) - Method in class net.sourceforge.czt.z2b.Z2B

Adds the string representionat of zName to the names list and a membership of zName in the given expression to the preds list.

declareVars(VarDecl, List<String>, List<Pred>) - Method in class net.sourceforge.czt.z2b.Z2B

Adds ALL the names in a VarDecl to the names/preds lists.

declareVars(List<NameTypePair>, List<String>, List<Pred>) - Method in class net.sourceforge.czt.z2b.Z2B

declareVars(NameSectTypeTriple, List<String>, List<Pred>) - Method in class net.sourceforge.czt.z2b.Z2B

DEFN_PREC - Static variable in class net.sourceforge.czt.z2b.BTermWriter

E

endPrec(int) - Method in class net.sourceforge.czt.z2b.BWriter

Ends an output region of a given precedence.

endPrec() - Method in class net.sourceforge.czt.z2b.BWriter

Start a new LOOSEST region without adding any "(".

endSection(String) - Method in class net.sourceforge.czt.z2b.BWriter

End the current section.

eqPred(ZName, Expr) - Static method in class net.sourceforge.czt.z2b.Create

Create an equality between a name and expression

F

foundInput - Variable in class net.sourceforge.czt.z2b.FreeVarChecker

foundOutput - Variable in class net.sourceforge.czt.z2b.FreeVarChecker

foundPrime - Variable in class net.sourceforge.czt.z2b.FreeVarChecker

FreeVarChecker - Class in net.sourceforge.czt.z2b

This class scans a Z predicate/expression to see if it contains various kinds of decorated variables.

FreeVarChecker() - Constructor for class net.sourceforge.czt.z2b.FreeVarChecker

G

getConstants() - Method in class net.sourceforge.czt.z2b.BMachine

Returns the constant 'Name's of this machine.

getDefns() - Method in class net.sourceforge.czt.z2b.BMachine

Stores all Name == Expr definitions.

getFactory() - Static method in class net.sourceforge.czt.z2b.Create

Returns the factory that is used to create various AST terms.

getInit() - Method in class net.sourceforge.czt.z2b.Classifier

getInitialisation() - Method in class net.sourceforge.czt.z2b.BMachine

Returns the initialisation predicates of this machine.

getInputs() - Method in class net.sourceforge.czt.z2b.BOperation

Returns the input names of this operation.

getInvariant() - Method in class net.sourceforge.czt.z2b.BMachine

Returns the invariant predicates

getOperations() - Method in class net.sourceforge.czt.z2b.BMachine

Returns the operations of this machine.

getOps() - Method in class net.sourceforge.czt.z2b.Classifier

getOutputs() - Method in class net.sourceforge.czt.z2b.BOperation

Returns the output names of this operation.

getPost() - Method in class net.sourceforge.czt.z2b.BOperation

Returns the postcondition predicates of the operation

getPre() - Method in class net.sourceforge.czt.z2b.BOperation

Returns the precondition predicates of the operation

getProperties() - Method in class net.sourceforge.czt.z2b.BMachine

Returns the properties of the constants

getSets() - Method in class net.sourceforge.czt.z2b.BMachine

Returns the sets used in this machine.

getSignature(NameSectTypeTriple) - Method in class net.sourceforge.czt.z2b.Z2B

Type is assumed to be of PowerType of SchemaType

getState() - Method in class net.sourceforge.czt.z2b.Classifier

getVariables() - Method in class net.sourceforge.czt.z2b.BMachine

Returns the state variables of this machine.

getVariables(SchExpr, Class<?>) - Method in class net.sourceforge.czt.z2b.Z2B

Assumes that all the declarations are VarDecls

I

infixOp(BTermWriter.BOperator, Term, Term) - Method in class net.sourceforge.czt.z2b.BTermWriter

This handles all infix operators (except '.').

L

lookup(NameSectTypeTriple) - Method in class net.sourceforge.czt.z2b.Z2B

LOOSEST - Static variable in class net.sourceforge.czt.z2b.BWriter

Minimum allowable precedence

M

machine - Variable in class net.sourceforge.czt.z2b.BOperation

The B machine that this operation belongs to

Main - Class in net.sourceforge.czt.z2b

Translate a Z specification from ZML format into B format.

Main() - Constructor for class net.sourceforge.czt.z2b.Main

main(String[]) - Static method in class net.sourceforge.czt.z2b.Main

makeBMachine(ZSect) - Method in class net.sourceforge.czt.z2b.Z2B

Translates a ZSect into a BMachine.

N

name - Variable in class net.sourceforge.czt.z2b.BOperation

The name of the operation

name_ - Variable in class net.sourceforge.czt.z2b.BMachine

The name of the machine

net.sourceforge.czt.z2b - package net.sourceforge.czt.z2b

nl() - Method in class net.sourceforge.czt.z2b.BWriter

Start a new line in the B file.

O

operation(NameSectTypeTriple) - Method in class net.sourceforge.czt.z2b.Z2B

P

precStack - Variable in class net.sourceforge.czt.z2b.BWriter

prime(String) - Static method in class net.sourceforge.czt.z2b.Create

Prime a Name

print(BWriter) - Method in class net.sourceforge.czt.z2b.BMachine

Prints the machine out to the given file, in *.mch syntax

print(BWriter) - Method in class net.sourceforge.czt.z2b.BOperation

Prints the operation out to the given file, in *.mch syntax

print(Term, String) - Method in class net.sourceforge.czt.z2b.Z2B

printAnyAssign(Map<String, ZName>, List<Pred>) - Method in class net.sourceforge.czt.z2b.BTermWriter

Print a non-deterministic update of some variables, given some predicates.

printAnyAssign(Map<String, ZName>, List<Pred>) - Method in class net.sourceforge.czt.z2b.BWriter

Print a non-deterministic update: ANY ..

printExpr(Expr) - Method in class net.sourceforge.czt.z2b.BTermWriter

Print a Z expression out in B syntax.

printExpr(Expr) - Method in class net.sourceforge.czt.z2b.BWriter

Print a Z expression out in B syntax.

printName(ZName) - Method in class net.sourceforge.czt.z2b.BWriter

Print one Z name into the current section.

printName(String) - Method in class net.sourceforge.czt.z2b.BWriter

Print one String name into the current section.

printNames(BWriter, List<String>) - Method in class net.sourceforge.czt.z2b.BMachine

Writes a list of names, separated by commas.

printNames(BWriter, Collection<String>) - Method in class net.sourceforge.czt.z2b.BOperation

Prints a list of names in concise format, separated by commas.

printPred(Pred) - Method in class net.sourceforge.czt.z2b.BTermWriter

Print a single Z predicate out in B syntax.

printPred(Pred) - Method in class net.sourceforge.czt.z2b.BWriter

Print a single Z predicate out in B syntax.

printPreds(List<Pred>) - Method in class net.sourceforge.czt.z2b.BTermWriter

Print a list of predicates, separated by '&' and newlines.

printPreds(List<Pred>) - Method in class net.sourceforge.czt.z2b.BWriter

Print a list of predicates, separated by '&' and newlines.

printSeparator(String) - Method in class net.sourceforge.czt.z2b.BWriter

Print a separator.

R

refExpr(ZName) - Static method in class net.sourceforge.czt.z2b.Create

Creates a RefExpr to a given Name

refName(String) - Static method in class net.sourceforge.czt.z2b.Create

Creates a Name from a String

refName(ZName) - Static method in class net.sourceforge.czt.z2b.Create

rename(Term) - Method in class net.sourceforge.czt.z2b.RenameVisitor

Apply this renaming to a Z term.

RenameVisitor - Class in net.sourceforge.czt.z2b

This class renames a given set of names.

RenameVisitor(Map<String, ZName>) - Constructor for class net.sourceforge.czt.z2b.RenameVisitor

Constructor for RenameVisitor

reset() - Method in class net.sourceforge.czt.z2b.FreeVarChecker

S

setFactory(ZFactory) - Static method in class net.sourceforge.czt.z2b.Create

Set the factory that is used to create various AST terms.

splitPrePost(Pred, List<Pred>, List<Pred>) - Method in class net.sourceforge.czt.z2b.Z2B

Split a complex postcondition predicate into pre/post lists.

splitSchText(ZSchText) - Method in class net.sourceforge.czt.z2b.BTermWriter

This prints a comma-separated list of all the names in a SchText, and returns the associated type conditions as one predicate.

startSection(String) - Method in class net.sourceforge.czt.z2b.BWriter

Start a new section/part of the B machine.

T

TIGHTEST - Static variable in class net.sourceforge.czt.z2b.BWriter

Maximum allowable precedence

U

unaryOp(BTermWriter.BOperator, Term) - Method in class net.sourceforge.czt.z2b.BTermWriter

This handles all unary functions: foo(Arg).

UnfoldException - Exception in net.sourceforge.czt.z2b

UnfoldException(Throwable) - Constructor for exception net.sourceforge.czt.z2b.UnfoldException

unprime(ZName) - Static method in class net.sourceforge.czt.z2b.Create

Unprime a name

V

visitAndPred(AndPred) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitApplExpr(ApplExpr) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitAxPara(AxPara) - Method in class net.sourceforge.czt.z2b.Z2B

Adds some axiomatic definitions to a B machine.

visitBindExpr(BindExpr) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitBindSelExpr(BindSelExpr) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitConjPara(ConjPara) - Method in class net.sourceforge.czt.z2b.Z2B

Ignore conjecture paragraphs.

visitConstDecl(ConstDecl) - Method in class net.sourceforge.czt.z2b.Z2B

visitExistsPred(ExistsPred) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitFalsePred(FalsePred) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitForallPred(ForallPred) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitFreePara(FreePara) - Method in class net.sourceforge.czt.z2b.Z2B

Process all free types.

visitFreetype(Freetype) - Method in class net.sourceforge.czt.z2b.Z2B

Adds a simple free type to a B machine.

visitGivenPara(GivenPara) - Method in class net.sourceforge.czt.z2b.Z2B

Adds all the given types to the 'parameters' list of a B machine.

visitIffPred(IffPred) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitImpliesPred(ImpliesPred) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitLambdaExpr(LambdaExpr) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitLatexMarkupPara(LatexMarkupPara) - Method in class net.sourceforge.czt.z2b.Z2B

Ignore Latex markup paragraphs.

visitListTerm(ListTerm<?>) - Method in class net.sourceforge.czt.z2b.Z2B

Visits a list term by visiting all its children.

visitMemPred(MemPred) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitName(Name) - Method in class net.sourceforge.czt.z2b.RenameVisitor

This visit method performs the renaming.

visitNarrPara(NarrPara) - Method in class net.sourceforge.czt.z2b.Z2B

Ignore narrative paragraphs.

visitNegPred(NegPred) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitNumExpr(NumExpr) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitOptempPara(OptempPara) - Method in class net.sourceforge.czt.z2b.Z2B

Ignore operator template paragraphs.

visitOrPred(OrPred) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitPowerExpr(PowerExpr) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitProdExpr(ProdExpr) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitRefExpr(RefExpr) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitSchExpr(SchExpr) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitSetCompExpr(SetCompExpr) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitSetExpr(SetExpr) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitTerm(Term) - Method in class net.sourceforge.czt.z2b.BTermWriter

This generic visit method recurses into all Z terms.

visitTerm(Term) - Method in class net.sourceforge.czt.z2b.FreeVarChecker

This generic visit method recurses into all Z terms.

visitTerm(Term) - Method in class net.sourceforge.czt.z2b.RenameVisitor

This generic visit method recurses into all Z terms.

visitTerm(Term) - Method in class net.sourceforge.czt.z2b.Z2B

This generic visit method is called whenever no other visit method matches the current term.

visitTruePred(TruePred) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitTupleExpr(TupleExpr) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitUnparsedPara(UnparsedPara) - Method in class net.sourceforge.czt.z2b.Z2B

Unparsed Z paragraphs cause the translaton to fail.

visitVarDecl(VarDecl) - Method in class net.sourceforge.czt.z2b.Z2B

visitZDeclList(ZDeclList) - Method in class net.sourceforge.czt.z2b.Z2B

visitZFreetypeList(ZFreetypeList) - Method in class net.sourceforge.czt.z2b.Z2B

visitZName(ZName) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitZName(ZName) - Method in class net.sourceforge.czt.z2b.FreeVarChecker

visitZNumeral(ZNumeral) - Method in class net.sourceforge.czt.z2b.BTermWriter

visitZParaList(ZParaList) - Method in class net.sourceforge.czt.z2b.Z2B

W

WHERE_PREC - Static variable in class net.sourceforge.czt.z2b.BTermWriter

Z

Z2B - Class in net.sourceforge.czt.z2b

This class converts a Z section into a B machine.

Z2B(SectionManager) - Constructor for class net.sourceforge.czt.z2b.Z2B

A B C D E F G I L M N O P R S T U V W Z