1 //
2 // THIS FILE IS AUTOMATICALLY GENERATED!!
3 //
4 // Generated at 2009-08-09 by the VDM++ to JAVA Code Generator
5 // (v8.2.1b - Wed 15-Jul-2009 14:09:22)
6 //
7 // Supported compilers: jdk 1.4/1.5/1.6
8 //
9
10 // ***** VDMTOOLS START Name=HeaderComment KEEP=NO
11 // ***** VDMTOOLS END Name=HeaderComment
12
13 // ***** VDMTOOLS START Name=package KEEP=NO
14 package org.overturetool.api.xml;
15
16 // ***** VDMTOOLS END Name=package
17
18 // ***** VDMTOOLS START Name=imports KEEP=NO
19
20 import jp.co.csk.vdm.toolbox.VDM.*;
21 import java.util.*;
22 // ***** VDMTOOLS END Name=imports
23
24
25
26 public class XmlAttribute {
27
28 // ***** VDMTOOLS START Name=vdmComp KEEP=NO
29 static UTIL.VDMCompare vdmComp = new UTIL.VDMCompare();
30 // ***** VDMTOOLS END Name=vdmComp
31
32 // ***** VDMTOOLS START Name=name KEEP=NO
33 public String name = null;
34 // ***** VDMTOOLS END Name=name
35
36 // ***** VDMTOOLS START Name=val KEEP=NO
37 public String val = null;
38 // ***** VDMTOOLS END Name=val
39
40
41 // ***** VDMTOOLS START Name=vdm_init_XmlAttribute KEEP=NO
42 private void vdm_init_XmlAttribute () throws CGException {
43 try {
44
45 name = new String("");
46 val = new String("");
47 }
48 catch (Exception e){
49
50 e.printStackTrace(System.out);
51 System.out.println(e.getMessage());
52 }
53 }
54 // ***** VDMTOOLS END Name=vdm_init_XmlAttribute
55
56
57 // ***** VDMTOOLS START Name=XmlAttribute KEEP=NO
58 public XmlAttribute () throws CGException {
59 vdm_init_XmlAttribute();
60 }
61 // ***** VDMTOOLS END Name=XmlAttribute
62
63
64 // ***** VDMTOOLS START Name=XmlAttribute#2|String|String KEEP=NO
65 public XmlAttribute (final String pname, final String pval) throws CGException {
66
67 vdm_init_XmlAttribute();
68 {
69
70 name = UTIL.ConvertToString(UTIL.clone(pname));
71 val = UTIL.ConvertToString(UTIL.clone(pval));
72 }
73 }
74 // ***** VDMTOOLS END Name=XmlAttribute#2|String|String
75
76
77 // ***** VDMTOOLS START Name=accept#1|XmlVisitor KEEP=NO
78 public void accept (final XmlVisitor pxv) throws CGException {
79 pxv.VisitXmlAttribute((XmlAttribute) this);
80 }
81 // ***** VDMTOOLS END Name=accept#1|XmlVisitor
82
83 }
84 ;