why3session.dtd 1.08 KB
Newer Older
1 2 3
<!ELEMENT why3session (file*)>
<!ATTLIST why3session name CDATA #REQUIRED>

MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
<!ELEMENT file (theory*)>
<!ATTLIST file name CDATA #REQUIRED>
<!ATTLIST file verified CDATA #REQUIRED>
7
<!ATTLIST file expanded CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
8 9 10 11

<!ELEMENT theory (goal*)>
<!ATTLIST theory name CDATA #REQUIRED>
<!ATTLIST theory verified CDATA #REQUIRED>
12
<!ATTLIST theory expanded CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
13 14 15 16 17

<!ELEMENT goal (proof*, transf*)>
<!ATTLIST goal name CDATA #REQUIRED>
<!ATTLIST goal expl CDATA #IMPLIED>
<!ATTLIST goal proved CDATA #REQUIRED>
18 19
<!ATTLIST goal sum CDATA #REQUIRED>
<!ATTLIST goal expanded CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
20

21
<!ELEMENT proof (result|undone)>
MARCHE Claude's avatar
MARCHE Claude committed
22
<!ATTLIST proof prover CDATA #REQUIRED>
23 24 25
<!ATTLIST proof timelimit CDATA #REQUIRED>
<!ATTLIST proof edited CDATA #IMPLIED>
<!ATTLIST proof obsolete CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
26 27 28 29 30

<!ELEMENT result EMPTY>
<!ATTLIST result status (valid|invalid|unknown|timeout|failure) #REQUIRED>
<!ATTLIST result time CDATA #IMPLIED>

31 32
<!ELEMENT undone EMPTY>

MARCHE Claude's avatar
MARCHE Claude committed
33 34 35
<!ELEMENT transf (goal*)>
<!ATTLIST transf name CDATA #REQUIRED>
<!ATTLIST transf proved CDATA #REQUIRED>
36
<!ATTLIST transf expanded CDATA #IMPLIED>