001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: /* Generated by Together */
012:
013: package de.uka.ilkd.key.logic;
014:
015: import java.io.IOException;
016: import java.io.StringWriter;
017:
018: import de.uka.ilkd.key.java.JavaProgramElement;
019: import de.uka.ilkd.key.java.NameAbstractionTable;
020: import de.uka.ilkd.key.java.PrettyPrinter;
021: import de.uka.ilkd.key.java.StatementBlock;
022:
023: public class JavaBlock {
024:
025: public static final JavaBlock EMPTY_JAVABLOCK = new JavaBlock();
026: private final JavaProgramElement prg;
027:
028: /** create a new empty JavaBlock as singleton
029: */
030: private JavaBlock() {
031: this .prg = null;
032: }
033:
034: /** create a new JavaBlock
035: * @param prg the root JavaProgramElement for this JavaBlock
036: */
037: private JavaBlock(JavaProgramElement prg) {
038: this .prg = prg;
039: }
040:
041: /** create a new JavaBlock
042: * @param prg the root StatementBlock for this JavaBlock.
043: * TacletIndex relies on <code>prg</code> being indeed a StatementBlock.
044: */
045: public static JavaBlock createJavaBlock(StatementBlock prg) {
046: if (prg == null) {
047: return EMPTY_JAVABLOCK;
048: }
049: return new JavaBlock(prg);
050:
051: }
052:
053: public boolean isEmpty() {
054: if ((program() instanceof StatementBlock)) {
055: return ((StatementBlock) program()).isEmpty();
056: }
057: return this == EMPTY_JAVABLOCK;
058: }
059:
060: public int size() {
061: if ((program() instanceof StatementBlock)) {
062: return ((StatementBlock) program()).getChildCount();
063: }
064: return 0;
065: }
066:
067: /** returns the hashCode */
068: public int hashCode() {
069: return 17 + ((program() == null) ? 0 : program().hashCode());
070: }
071:
072: /** returns true iff the program elements are equal */
073: public boolean equals(Object o) {
074: if (o == this ) {
075: return true;
076: } else if (!(o instanceof JavaBlock)) {
077: return false;
078: }
079: return ((JavaBlock) o).program().equals(program());
080: }
081:
082: /** returns true if the given ProgramElement is equal to the
083: * one of the JavaBlock modulo renaming (see comment in SourceElement)
084: */
085: public boolean equalsModRenaming(Object o, NameAbstractionTable nat) {
086: if (!(o instanceof JavaBlock)) {
087: return false;
088: }
089: return equalsModRenaming(((JavaBlock) o).program(), nat);
090: }
091:
092: /** returns true if the given ProgramElement is equal to the
093: * one of the JavaBlock modulo renaming (see comment in SourceElement)
094: */
095: private boolean equalsModRenaming(JavaProgramElement pe,
096: NameAbstractionTable nat) {
097: if (pe == null && program() == null) {
098: return true;
099: } else if (pe != null && program() != null) {
100: return program().equalsModRenaming(pe, nat);
101: }
102: return false;
103: }
104:
105: /** returns the java program
106: * @return the stored JavaProgramElement
107: */
108: public JavaProgramElement program() {
109: return prg;
110: }
111:
112: /** toString */
113: public String toString() {
114: if (this == EMPTY_JAVABLOCK)
115: return "";
116: StringWriter sw = new StringWriter();
117: try {
118: PrettyPrinter pp = new PrettyPrinter(sw, true);
119: pp.setIndentationLevel(0);
120: prg.prettyPrint(pp);
121: } catch (IOException e) {
122: System.err.println("toString of JavaBlock failed due to :"
123: + e);
124: e.printStackTrace();
125: }
126: return sw.toString();
127: }
128:
129: }
|