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  JMLMethodSpeccloneFor(ProgramMethod method, JMLClassSpec jmlClassSpec)
     This is used for modelling specification inheritance for overwriten methods.
public  JMLMethodSpeccopy()
    
protected  TermcreateModalityTermForEnsures(Term post, boolean desugar, boolean withInv, boolean allInv)
    
public  ProgramElementgetProofStatement()
    
public  StringtoString()
    


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)

www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.