Java Doc for JMLNormalMethodSpec.java in  » Testing » KeY » de » uka » ilkd » key » jml » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation 1.  6.0 JDK Core 2.  6.0 JDK Modules 3.  6.0 JDK Modules com.sun 4.  6.0 JDK Modules com.sun.java 5.  6.0 JDK Modules sun 6.  6.0 JDK Platform 7.  Ajax 8.  Apache Harmony Java SE 9.  Aspect oriented 10.  Authentication Authorization 11.  Blogger System 12.  Build 13.  Byte Code 14.  Cache 15.  Chart 16.  Chat 17.  Code Analyzer 18.  Collaboration 19.  Content Management System 20.  Database Client 21.  Database DBMS 22.  Database JDBC Connection Pool 23.  Database ORM 24.  Development 25.  EJB Server geronimo 26.  EJB Server GlassFish 27.  EJB Server JBoss 4.2.1 28.  EJB Server resin 3.1.5 29.  ERP CRM Financial 30.  ESB 31.  Forum 32.  GIS 33.  Graphic Library 34.  Groupware 35.  HTML Parser 36.  IDE 37.  IDE Eclipse 38.  IDE Netbeans 39.  Installer 40.  Internationalization Localization 41.  Inversion of Control 42.  Issue Tracking 43.  J2EE 44.  JBoss 45.  JMS 46.  JMX 47.  Library 48.  Mail Clients 49.  Net 50.  Parser 51.  PDF 52.  Portal 53.  Profiler 54.  Project Management 55.  Report 56.  RSS RDF 57.  Rule Engine 58.  Science 59.  Scripting 60.  Search Engine 61.  Security 62.  Sevlet Container 63.  Source Control 64.  Swing Library 65.  Template Engine 66.  Test Coverage 67.  Testing 68.  UML 69.  Web Crawler 70.  Web Framework 71.  Web Mail 72.  Web Server 73.  Web Services 74.  Web Services apache cxf 2.0.1 75.  Web Services AXIS2 76.  Wiki Engine 77.  Workflow Engines 78.  XML 79.  XML UI Java Java Tutorial Java Open Source Jar File Download Java Articles Java Products Java by API Photoshop Tutorials Maya Tutorials Flash Tutorials 3ds-Max Tutorials Illustrator Tutorials GIMP Tutorials C# / C Sharp C# / CSharp Tutorial C# / CSharp Open Source ASP.Net ASP.NET Tutorial JavaScript DHTML JavaScript Tutorial JavaScript Reference HTML / CSS HTML CSS Reference C / ANSI-C C Tutorial C++ C++ Tutorial Ruby PHP Python Python Tutorial Python Open Source SQL Server / T-SQL SQL Server / T-SQL Tutorial Oracle PL / SQL Oracle PL/SQL Tutorial PostgreSQL SQL / MySQL MySQL Tutorial VB.Net VB.Net Tutorial Flash / Flex / ActionScript VBA / Excel / Access / Word XML XML Tutorial Microsoft Office PowerPoint 2007 Tutorial Microsoft Office Excel 2007 Tutorial Microsoft Office Word 2007 Tutorial

Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.jml   Source Cross Reference   Class Diagram   Java Document (Java Doc)   de.uka.ilkd.key.jml.JMLSpec    de.uka.ilkd.key.jml.JMLMethodSpec       de.uka.ilkd.key.jml.JMLNormalMethodSpec JMLNormalMethodSpec public class JMLNormalMethodSpec extends JMLMethodSpec (Code) A normal jml methodspecification declared by the jml-keyword normal_behavior Constructor Summary public   JMLNormalMethodSpec(ProgramMethod pm, Services services, Namespace params, LinkedHashMap term2old, JMLClassSpec cSpec, NamespaceSet nss, String javaPath)      protected   JMLNormalMethodSpec()      Method Summary public  JMLMethodSpec cloneFor(ProgramMethod method, JMLClassSpec jmlClassSpec)      This is used for modelling specification inheritance for overwriten methods. public  JMLMethodSpec copy()      protected  Term createModalityTermForEnsures(Term post, boolean desugar, boolean withInv, boolean allInv)      public  ProgramElement getProofStatement()      public  String toString()      Constructor Detail JMLNormalMethodSpec public JMLNormalMethodSpec(ProgramMethod pm, Services services, Namespace params, LinkedHashMap term2old, JMLClassSpec cSpec, NamespaceSet nss, String javaPath)(Code) JMLNormalMethodSpec protected JMLNormalMethodSpec()(Code) Method Detail cloneFor public JMLMethodSpec cloneFor(ProgramMethod method, JMLClassSpec jmlClassSpec)(Code) This is used for modelling specification inheritance for overwriten methods. copy public JMLMethodSpec copy()(Code) createModalityTermForEnsures protected Term createModalityTermForEnsures(Term post, boolean desugar, boolean withInv, boolean allInv)(Code) getProofStatement public ProgramElement getProofStatement()(Code) toString public String toString()(Code) Fields inherited from de.uka.ilkd.key.jml.JMLMethodSpec protected static Term BOOL_FALSE(Code)(Java Doc) protected static Term BOOL_TRUE(Code)(Java Doc) final public static String EVERYTHING(Code)(Java Doc) protected String assignableMode(Code)(Java Doc) protected SetOfLocationDescriptor assignableVariables(Code)(Java Doc) protected JMLClassSpec cSpec(Code)(Java Doc) protected TypeDeclaration cd(Code)(Java Doc) protected Term diverges(Code)(Java Doc) protected KeYJavaType exc(Code)(Java Doc) protected static int excCondCount(Code)(Java Doc) protected ProgramVariable excVar(Code)(Java Doc) protected static int exceptionVarCount(Code)(Java Doc) protected int id(Code)(Java Doc) protected String inhFrom(Code)(Java Doc) protected ReferencePrefix inheritedPrefix(Code)(Java Doc) protected JavaInfo ji(Code)(Java Doc) protected static int logicVarCount(Code)(Java Doc) protected TreeMap lv2old(Code)(Java Doc) protected StatementBlock mBS(Code)(Java Doc) protected LinkedHashMap modalityTermForEnsuresCache(Code)(Java Doc) protected NamespaceSet nss(Code)(Java Doc) protected static Term nullTerm(Code)(Java Doc) protected Namespace params(Code)(Java Doc) protected ProgramMethod pm(Code)(Java Doc) protected ProgramVariable resultVar(Code)(Java Doc) protected static int resultVarCount(Code)(Java Doc) protected ProgramVariable self(Code)(Java Doc) protected Services services(Code)(Java Doc) protected SetOfSignals signals(Code)(Java Doc) protected boolean staticInit(Code)(Java Doc) protected TermBuilder tb(Code)(Java Doc) protected LinkedHashMap term2old(Code)(Java Doc) Methods inherited from de.uka.ilkd.key.jml.JMLMethodSpec public void addAssignable(SetOfLocationDescriptor locations)(Code)(Java Doc) public void addDiverges(Term t)(Code)(Java Doc) public static Term addOldQuantifiers(Term a, Map term2old, boolean useQuantifiers, Namespace params)(Code)(Java Doc) public void addPost(Term t)(Code)(Java Doc) public void addPre(Term t)(Code)(Java Doc) public void addSignals(KeYJavaType exc, ProgramVariable v, Term cond)(Code)(Java Doc) public Term bindSpecVars(Term t)(Code)(Java Doc) protected JavaBlock catchAllJB(boolean desugar)(Code)(Java Doc) public void clearModalityTermForEnsuresCache()(Code)(Java Doc) public JMLMethodSpec cloneFor(ProgramMethod pm, JMLClassSpec cSpec)(Code)(Java Doc) protected JMLMethodSpec cloneForHelper(JMLMethodSpec clone, ProgramMethod pm, JMLClassSpec cSpec)(Code)(Java Doc) public boolean containsQuantifiedAssignableLocation()(Code)(Java Doc) public JMLMethodSpec copy()(Code)(Java Doc) protected JMLMethodSpec copyHelper(JMLMethodSpec copy)(Code)(Java Doc) public Term createDLFormula(boolean withPostInvariant, boolean allInvariants)(Code)(Java Doc) protected Term createDiverges()(Code)(Java Doc) protected static Term createEqualityTermForOldLV(Term t, Term old, LinkedList l, LinkedList oldFS, Map lv2old)(Code)(Java Doc) protected Term createModalityTermForEnsures(Term post, boolean desugar, boolean withInv, boolean allInv)(Code)(Java Doc) public SetOfLocationDescriptor getAssignable()(Code)(Java Doc) public String getAssignableMode()(Code)(Java Doc) public CatchAllStatement getCatchAllStatement()(Code)(Java Doc) public TypeDeclaration getClassDeclaration()(Code)(Java Doc) public Term getCompletePost(boolean withClassSpec, boolean allInv)(Code)(Java Doc) public Term getCompletePostFunctional(boolean withClassSpec, boolean allInv)(Code)(Java Doc) public Term getCompletePre(boolean withClassSpec, boolean allInv, boolean terminationCase)(Code)(Java Doc) public ProgramVariable getExceptionVariable()(Code)(Java Doc) public ReferencePrefix getInheritedPrefix()(Code)(Java Doc) public String getJavaPath()(Code)(Java Doc) public Map getLv2Const()(Code)(Java Doc) public MethodDeclaration getMethodDeclaration()(Code)(Java Doc) public JavaModelMethod getModelMethod()(Code)(Java Doc) public NamespaceSet getNamespaces()(Code)(Java Doc) public ListOfOperator getOldFuncSymbols()(Code)(Java Doc) public ListOfQuantifierPrefixEntry getOldLVs()(Code)(Java Doc) public ProgramVariable getParameterAt(int i)(Code)(Java Doc) public Term getPi1()(Code)(Java Doc) public Term getPi1Functional()(Code)(Java Doc) public Term getPost()(Code)(Java Doc) public Term getPre()(Code)(Java Doc) public ReferencePrefix getPrefix()(Code)(Java Doc) public ProgramMethod getProgramMethod()(Code)(Java Doc) public ProgramElement getProofStatement()(Code)(Java Doc) public ProgramVariable getResultVar()(Code)(Java Doc) public ProgramVariable getSelf()(Code)(Java Doc) public Services getServices()(Code)(Java Doc) public SetOfSignals getSignals()(Code)(Java Doc) public ListOfNamed getSpecVars()(Code)(Java Doc) public LinkedHashMap getTerm2Old()(Code)(Java Doc) public int id()(Code)(Java Doc) public Collection introducedConstants()(Code)(Java Doc) public boolean isCloneableFor(ProgramMethod method)(Code)(Java Doc) public StatementBlock makeMBS()(Code)(Java Doc) public Term replaceFreeVarsWithConsts(Term t)(Code)(Java Doc) public SetOfLocationDescriptor replaceModelFieldsInAssignable()(Code)(Java Doc) public SetOfLocationDescriptor replaceModelFieldsInAssignable(JMLClassSpec cs)(Code)(Java Doc) public void setAssignableMode(String s)(Code)(Java Doc) public void setId(int id)(Code)(Java Doc) public void setSpecVars(ListOfNamed svs)(Code)(Java Doc) public boolean terminates()(Code)(Java Doc) public String toString()(Code)(Java Doc) protected String toStringHelper(String s)(Code)(Java Doc) protected Term updateParameters(ArrayOfParameterDeclaration oldParams, ArrayOfParameterDeclaration newParams, Term target)(Code)(Java Doc) protected Term updatePrefix(Term t)(Code)(Java Doc) Fields inherited from de.uka.ilkd.key.jml.JMLSpec protected Namespace funcNS(Code)(Java Doc) protected NotSupportedExpressionException nsEx(Code)(Java Doc) protected Namespace progVarNS(Code)(Java Doc) Methods inherited from de.uka.ilkd.key.jml.JMLSpec public Namespace getFunctionNS()(Code)(Java Doc) public Namespace getProgramVariableNS()(Code)(Java Doc) abstract public LinkedHashMap getTerm2Old()(Code)(Java Doc) public boolean isValid()(Code)(Java Doc) public void setInvalid(NotSupportedExpressionException nsEx)(Code)(Java Doc)