01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10: package de.uka.ilkd.key.java;
11:
12: import java.util.Iterator;
13: import java.util.LinkedList;
14: import java.util.List;
15:
16: /**
17: * This class is used for the equals modulo renaming method in
18: * SourceElement. The purpose of this class is to abstract from
19: * names. Therefore it represents a mapping o1 x o2 -> abstractName
20: * where o1, o2 are of the same type (Label or ProgramVariable). The
21: * objectif is that the comparing method uses this new name for o1 and
22: * o2 instead of their real name. For this comparision a method is
23: * offered so that the assigned name is not given outside.
24: */
25: public class NameAbstractionTable {
26:
27: /**
28: * The order in which symbols are declared in the two terms or programs that
29: * are compared. The latest declaration of a symbol will be the first
30: * matching entry in the list
31: */
32: private List declarations0 = null, declarations1 = null;
33:
34: /**
35: * adds the given two elements to the table
36: * @param pe1 SourceElement to be added
37: * @param pe2 SourceElement to be added
38: */
39: public void add(SourceElement pe1, SourceElement pe2) {
40: if (declarations0 == null) {
41: declarations0 = new LinkedList();
42: declarations1 = new LinkedList();
43: }
44:
45: declarations0.add(0, pe1);
46: declarations1.add(0, pe2);
47: }
48:
49: /**
50: * tests if the given elements have been assigned to the same
51: * abstract name.
52: * @param pe1 SourceElement
53: * @param pe2 SourceElement
54: * @returns true if the pe1 and pe2 have been assigned to the same
55: * name
56: */
57: public boolean sameAbstractName(SourceElement pe0, SourceElement pe1) {
58: if (declarations0 != null) {
59: final Iterator it0 = declarations0.iterator();
60: final Iterator it1 = declarations1.iterator();
61:
62: while (it0.hasNext()) {
63: // both lists are assumed to hold the same number of elements
64: final Object o0 = it0.next();
65: final Object o1 = it1.next();
66:
67: if (pe0.equals(o0)) {
68: return pe1.equals(o1);
69: } else if (pe1.equals(o1)) {
70: return false;
71: }
72: }
73: }
74:
75: return pe0.equals(pe1);
76: }
77:
78: }
|