net.sourceforge.czt.z2b

Class Z2B

java.lang.Object

net.sourceforge.czt.z2b.Z2B

All Implemented Interfaces:

net.sourceforge.czt.base.visitor.ListTermVisitor<Object>, net.sourceforge.czt.base.visitor.TermVisitor<Object>, net.sourceforge.czt.util.Visitor<Object>, net.sourceforge.czt.z.visitor.AxParaVisitor<Object>, net.sourceforge.czt.z.visitor.ConjParaVisitor<Object>, net.sourceforge.czt.z.visitor.ConstDeclVisitor<Object>, net.sourceforge.czt.z.visitor.FreeParaVisitor<Object>, net.sourceforge.czt.z.visitor.FreetypeVisitor<Object>, net.sourceforge.czt.z.visitor.GivenParaVisitor<Object>, net.sourceforge.czt.z.visitor.LatexMarkupParaVisitor<Object>, net.sourceforge.czt.z.visitor.NarrParaVisitor<Object>, net.sourceforge.czt.z.visitor.OptempParaVisitor<Object>, net.sourceforge.czt.z.visitor.UnparsedParaVisitor<Object>, net.sourceforge.czt.z.visitor.VarDeclVisitor<Object>, net.sourceforge.czt.z.visitor.ZDeclListVisitor<Object>, net.sourceforge.czt.z.visitor.ZFreetypeListVisitor<Object>, net.sourceforge.czt.z.visitor.ZParaListVisitor<Object>

public class Z2B
extends Object
implements net.sourceforge.czt.base.visitor.TermVisitor<Object>, net.sourceforge.czt.base.visitor.ListTermVisitor<Object>, net.sourceforge.czt.z.visitor.LatexMarkupParaVisitor<Object>, net.sourceforge.czt.z.visitor.GivenParaVisitor<Object>, net.sourceforge.czt.z.visitor.FreeParaVisitor<Object>, net.sourceforge.czt.z.visitor.FreetypeVisitor<Object>, net.sourceforge.czt.z.visitor.AxParaVisitor<Object>, net.sourceforge.czt.z.visitor.ConjParaVisitor<Object>, net.sourceforge.czt.z.visitor.NarrParaVisitor<Object>, net.sourceforge.czt.z.visitor.OptempParaVisitor<Object>, net.sourceforge.czt.z.visitor.UnparsedParaVisitor<Object>, net.sourceforge.czt.z.visitor.VarDeclVisitor<Object>, net.sourceforge.czt.z.visitor.ConstDeclVisitor<Object>, net.sourceforge.czt.z.visitor.ZDeclListVisitor<Object>, net.sourceforge.czt.z.visitor.ZParaListVisitor<Object>, net.sourceforge.czt.z.visitor.ZFreetypeListVisitor<Object>

This class converts a Z section into a B machine.

Author:

Mark Utting

Constructor Summary

Constructors

Constructor and Description
Z2B(net.sourceforge.czt.session.SectionManager manager)

Method Summary

Modifier and Type	Method and Description
protected void	addPred(net.sourceforge.czt.z.ast.Pred pred, List<net.sourceforge.czt.z.ast.Pred> preds) Flatten conjuncts and add them to the given list.
protected void	addPreds(List<net.sourceforge.czt.z.ast.Pred> inpreds, List<net.sourceforge.czt.z.ast.Pred> preds) Apply addPred to a LIST of predicates.
protected void	declareVar(net.sourceforge.czt.z.ast.ZName zName, net.sourceforge.czt.z.ast.Expr expr, List<String> names, List<net.sourceforge.czt.z.ast.Pred> preds) Adds the string representionat of zName to the names list and a membership of zName in the given expression to the preds list.
protected void	declareVars(List<net.sourceforge.czt.z.ast.NameTypePair> vars, List<String> names, List<net.sourceforge.czt.z.ast.Pred> preds)
protected void	declareVars(net.sourceforge.czt.z.ast.NameSectTypeTriple triple, List<String> names, List<net.sourceforge.czt.z.ast.Pred> preds)
protected void	declareVars(net.sourceforge.czt.z.ast.VarDecl decl, List<String> names, List<net.sourceforge.czt.z.ast.Pred> preds) Adds ALL the names in a VarDecl to the names/preds lists.
protected net.sourceforge.czt.z.ast.Signature	getSignature(net.sourceforge.czt.z.ast.NameSectTypeTriple triple) Type is assumed to be of PowerType of SchemaType
protected Map<net.sourceforge.czt.z.ast.ZName,net.sourceforge.czt.z.ast.Expr>	getVariables(net.sourceforge.czt.z.ast.SchExpr schExpr, Class<?> decor) Assumes that all the declarations are VarDecls
protected net.sourceforge.czt.z.ast.Expr	lookup(net.sourceforge.czt.z.ast.NameSectTypeTriple triple)
BMachine	makeBMachine(net.sourceforge.czt.z.ast.ZSect sect) Translates a ZSect into a BMachine.
protected BOperation	operation(net.sourceforge.czt.z.ast.NameSectTypeTriple triple)
protected void	print(net.sourceforge.czt.base.ast.Term term, String section)
protected void	splitPrePost(net.sourceforge.czt.z.ast.Pred pred, List<net.sourceforge.czt.z.ast.Pred> pre, List<net.sourceforge.czt.z.ast.Pred> post) Split a complex postcondition predicate into pre/post lists.
Object	visitAxPara(net.sourceforge.czt.z.ast.AxPara para) Adds some axiomatic definitions to a B machine.
Object	visitConjPara(net.sourceforge.czt.z.ast.ConjPara para) Ignore conjecture paragraphs.
Object	visitConstDecl(net.sourceforge.czt.z.ast.ConstDecl decl)
Object	visitFreePara(net.sourceforge.czt.z.ast.FreePara para) Process all free types.
Object	visitFreetype(net.sourceforge.czt.z.ast.Freetype freetype) Adds a simple free type to a B machine.
Object	visitGivenPara(net.sourceforge.czt.z.ast.GivenPara para) Adds all the given types to the 'parameters' list of a B machine.
Object	visitLatexMarkupPara(net.sourceforge.czt.z.ast.LatexMarkupPara para) Ignore Latex markup paragraphs.
Object	visitListTerm(net.sourceforge.czt.base.ast.ListTerm<?> term) Visits a list term by visiting all its children.
Object	visitNarrPara(net.sourceforge.czt.z.ast.NarrPara para) Ignore narrative paragraphs.
Object	visitOptempPara(net.sourceforge.czt.z.ast.OptempPara para) Ignore operator template paragraphs.
Object	visitTerm(net.sourceforge.czt.base.ast.Term term) This generic visit method is called whenever no other visit method matches the current term.
Object	visitUnparsedPara(net.sourceforge.czt.z.ast.UnparsedPara para) Unparsed Z paragraphs cause the translaton to fail.
Object	visitVarDecl(net.sourceforge.czt.z.ast.VarDecl decl)
Object	visitZDeclList(net.sourceforge.czt.z.ast.ZDeclList zDeclList)
Object	visitZFreetypeList(net.sourceforge.czt.z.ast.ZFreetypeList list)
Object	visitZParaList(net.sourceforge.czt.z.ast.ZParaList list)

Methods inherited from class java.lang.Object

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

Constructor Detail

Z2B

public Z2B(net.sourceforge.czt.session.SectionManager manager)
    throws UnfoldException

Throws:

UnfoldException

Method Detail

makeBMachine

public BMachine makeBMachine(net.sourceforge.czt.z.ast.ZSect sect)
                      throws BException,
                             net.sourceforge.czt.session.CommandException

Translates a ZSect into a BMachine.

Parameters:

sect - the ZSect to be translated requires varExtract != null

Throws:

BException

net.sourceforge.czt.session.CommandException

getSignature

protected net.sourceforge.czt.z.ast.Signature getSignature(net.sourceforge.czt.z.ast.NameSectTypeTriple triple)

Type is assumed to be of PowerType of SchemaType

lookup

protected net.sourceforge.czt.z.ast.Expr lookup(net.sourceforge.czt.z.ast.NameSectTypeTriple triple)
                                         throws net.sourceforge.czt.session.CommandException

Throws:

net.sourceforge.czt.session.CommandException

print

protected void print(net.sourceforge.czt.base.ast.Term term,
                     String section)
              throws net.sourceforge.czt.print.util.PrintException

Throws:

net.sourceforge.czt.print.util.PrintException

getVariables

protected Map<net.sourceforge.czt.z.ast.ZName,net.sourceforge.czt.z.ast.Expr> getVariables(net.sourceforge.czt.z.ast.SchExpr schExpr,
                                                                                           Class<?> decor)

Assumes that all the declarations are VarDecls

operation

protected BOperation operation(net.sourceforge.czt.z.ast.NameSectTypeTriple triple)
                        throws net.sourceforge.czt.session.CommandException

Throws:

net.sourceforge.czt.session.CommandException

declareVar

protected void declareVar(net.sourceforge.czt.z.ast.ZName zName,
                          net.sourceforge.czt.z.ast.Expr expr,
                          List<String> names,
                          List<net.sourceforge.czt.z.ast.Pred> preds)

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

declareVars

protected void declareVars(net.sourceforge.czt.z.ast.VarDecl decl,
                           List<String> names,
                           List<net.sourceforge.czt.z.ast.Pred> preds)

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

declareVars

protected void declareVars(List<net.sourceforge.czt.z.ast.NameTypePair> vars,
                           List<String> names,
                           List<net.sourceforge.czt.z.ast.Pred> preds)

declareVars

protected void declareVars(net.sourceforge.czt.z.ast.NameSectTypeTriple triple,
                           List<String> names,
                           List<net.sourceforge.czt.z.ast.Pred> preds)
                    throws net.sourceforge.czt.session.CommandException

Throws:

net.sourceforge.czt.session.CommandException

addPred

protected void addPred(net.sourceforge.czt.z.ast.Pred pred,
                       List<net.sourceforge.czt.z.ast.Pred> preds)

Flatten conjuncts and add them to the given list.

addPreds

protected void addPreds(List<net.sourceforge.czt.z.ast.Pred> inpreds,
                        List<net.sourceforge.czt.z.ast.Pred> preds)

Apply addPred to a LIST of predicates.

splitPrePost

protected void splitPrePost(net.sourceforge.czt.z.ast.Pred pred,
                            List<net.sourceforge.czt.z.ast.Pred> pre,
                            List<net.sourceforge.czt.z.ast.Pred> post)

Split a complex postcondition predicate into pre/post lists. This currently uses a very simplistic algorithm. It splits post into conjuncts and puts all conjuncts that do not involve primed or output variables into 'pre', and all remaining conjuncts into 'post'. This is not always correct, since some conjuncts that involve primes/outputs may add implicit constraints on inputs. TODO: improve the algorithm further.

visitTerm

public Object visitTerm(net.sourceforge.czt.base.ast.Term term)

This generic visit method is called whenever no other visit method matches the current term. Since we want to explicitly handle each kind of top-level term, we throw an exception to report unexpected kinds of terms.

Specified by:

visitTerm in interface net.sourceforge.czt.base.visitor.TermVisitor<Object>

visitListTerm

public Object visitListTerm(net.sourceforge.czt.base.ast.ListTerm<?> term)

Visits a list term by visiting all its children.

Specified by:

visitListTerm in interface net.sourceforge.czt.base.visitor.ListTermVisitor<Object>

visitZParaList

public Object visitZParaList(net.sourceforge.czt.z.ast.ZParaList list)

Specified by:

visitZParaList in interface net.sourceforge.czt.z.visitor.ZParaListVisitor<Object>

visitGivenPara

public Object visitGivenPara(net.sourceforge.czt.z.ast.GivenPara para)

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

Specified by:

visitGivenPara in interface net.sourceforge.czt.z.visitor.GivenParaVisitor<Object>

visitFreePara

public Object visitFreePara(net.sourceforge.czt.z.ast.FreePara para)

Process all free types.

Specified by:

visitFreePara in interface net.sourceforge.czt.z.visitor.FreeParaVisitor<Object>

visitZFreetypeList

public Object visitZFreetypeList(net.sourceforge.czt.z.ast.ZFreetypeList list)

Specified by:

visitZFreetypeList in interface net.sourceforge.czt.z.visitor.ZFreetypeListVisitor<Object>

visitLatexMarkupPara

public Object visitLatexMarkupPara(net.sourceforge.czt.z.ast.LatexMarkupPara para)

Ignore Latex markup paragraphs.

Specified by:

visitLatexMarkupPara in interface net.sourceforge.czt.z.visitor.LatexMarkupParaVisitor<Object>

visitFreetype

public Object visitFreetype(net.sourceforge.czt.z.ast.Freetype freetype)

Adds a simple free type to a B machine.

Specified by:

visitFreetype in interface net.sourceforge.czt.z.visitor.FreetypeVisitor<Object>

visitAxPara

public Object visitAxPara(net.sourceforge.czt.z.ast.AxPara para)

Adds some axiomatic definitions to a B machine.

Specified by:

visitAxPara in interface net.sourceforge.czt.z.visitor.AxParaVisitor<Object>

visitZDeclList

public Object visitZDeclList(net.sourceforge.czt.z.ast.ZDeclList zDeclList)

Specified by:

visitZDeclList in interface net.sourceforge.czt.z.visitor.ZDeclListVisitor<Object>

visitConjPara

public Object visitConjPara(net.sourceforge.czt.z.ast.ConjPara para)

Ignore conjecture paragraphs.

Specified by:

visitConjPara in interface net.sourceforge.czt.z.visitor.ConjParaVisitor<Object>

visitNarrPara

public Object visitNarrPara(net.sourceforge.czt.z.ast.NarrPara para)

Ignore narrative paragraphs.

Specified by:

visitNarrPara in interface net.sourceforge.czt.z.visitor.NarrParaVisitor<Object>

visitOptempPara

public Object visitOptempPara(net.sourceforge.czt.z.ast.OptempPara para)

Ignore operator template paragraphs.

Specified by:

visitOptempPara in interface net.sourceforge.czt.z.visitor.OptempParaVisitor<Object>

visitUnparsedPara

public Object visitUnparsedPara(net.sourceforge.czt.z.ast.UnparsedPara para)

Unparsed Z paragraphs cause the translaton to fail.

Specified by:

visitUnparsedPara in interface net.sourceforge.czt.z.visitor.UnparsedParaVisitor<Object>

visitVarDecl

public Object visitVarDecl(net.sourceforge.czt.z.ast.VarDecl decl)

Specified by:

visitVarDecl in interface net.sourceforge.czt.z.visitor.VarDeclVisitor<Object>

visitConstDecl

public Object visitConstDecl(net.sourceforge.czt.z.ast.ConstDecl decl)

Specified by:

visitConstDecl in interface net.sourceforge.czt.z.visitor.ConstDeclVisitor<Object>