why3session.dtd 1.73 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
<!ELEMENT why3session (prover*, file*)>
2 3
<!ATTLIST why3session name CDATA #REQUIRED>

MARCHE Claude's avatar
MARCHE Claude committed
4 5 6 7 8
<!ELEMENT prover EMPTY>
<!ATTLIST prover id CDATA #REQUIRED>
<!ATTLIST prover name CDATA #REQUIRED>
<!ATTLIST prover version CDATA #REQUIRED>

MARCHE Claude's avatar
MARCHE Claude committed
9 10 11
<!ELEMENT file (theory*)>
<!ATTLIST file name CDATA #REQUIRED>
<!ATTLIST file verified CDATA #REQUIRED>
12
<!ATTLIST file expanded CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
13

MARCHE Claude's avatar
MARCHE Claude committed
14
<!ELEMENT theory (label*,goal*)>
MARCHE Claude's avatar
MARCHE Claude committed
15 16
<!ATTLIST theory name CDATA #REQUIRED>
<!ATTLIST theory verified CDATA #REQUIRED>
17
<!ATTLIST theory expanded CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
18 19 20 21
<!ATTLIST theory locfile CDATA #IMPLIED>
<!ATTLIST theory loclnum CDATA #IMPLIED>
<!ATTLIST theory loccnumb CDATA #IMPLIED>
<!ATTLIST theory loccnume CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
22

MARCHE Claude's avatar
MARCHE Claude committed
23
<!ELEMENT goal (label*, proof*, transf*)>
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26
<!ATTLIST goal name CDATA #REQUIRED>
<!ATTLIST goal expl CDATA #IMPLIED>
<!ATTLIST goal proved CDATA #REQUIRED>
27
<!ATTLIST goal sum CDATA #REQUIRED>
MARCHE Claude's avatar
MARCHE Claude committed
28
<!ATTLIST goal shape CDATA #IMPLIED>
29
<!ATTLIST goal expanded CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
30 31 32 33
<!ATTLIST goal locfile CDATA #IMPLIED>
<!ATTLIST goal loclnum CDATA #IMPLIED>
<!ATTLIST goal loccnumb CDATA #IMPLIED>
<!ATTLIST goal loccnume CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
34

35
<!ELEMENT proof (result|undone)>
MARCHE Claude's avatar
MARCHE Claude committed
36
<!ATTLIST proof prover CDATA #REQUIRED>
37 38
<!ATTLIST proof timelimit CDATA #IMPLIED>
<!ATTLIST proof memlimit CDATA #IMPLIED>
39 40
<!ATTLIST proof edited CDATA #IMPLIED>
<!ATTLIST proof obsolete CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
41
<!ATTLIST proof archived CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
42 43 44 45 46

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

47 48
<!ELEMENT undone EMPTY>

MARCHE Claude's avatar
MARCHE Claude committed
49 50 51
<!ELEMENT transf (goal*)>
<!ATTLIST transf name CDATA #REQUIRED>
<!ATTLIST transf proved CDATA #REQUIRED>
52
<!ATTLIST transf expanded CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
53 54 55

<!ELEMENT label EMPTY>
<!ATTLIST label name CDATA #REQUIRED>