fmrisc.Communication
Class Store

java.lang.Object
  fmrisc.Communication.Store

public final class Store
extends java.lang.Object

Persistent store of declarations and proofs. For a declaration of (where in {type,value,formula}) the following files are created: __decl.xgz Gzipped XML file holding the OMDoc representation of the declaration. __hash.txt (not for proofs) A single text line with a hash value for the representation (a non-negative integer number in decimal representation). __time.txt A single text line with a time stamp (a non-negative integer number in decimal representation). __refs.xml XML file representing the symbols referenced in the declaration: time="timestampvalue">> ... Writing to the Store: If an entity is to be written to the store, it is assumed that all the symbols it depends on have already been updated in the store. If the entity is not yet contained in the store, we write it to the store and are done. Otherwise, we check whether the symbols listed in the corresponding "refs" file are stored with the same time stamps as listed in the file. If yes, then the hash value of the internal representation is computed. If this value is the same as the hash value of the "hash" file, we assume that the definition has not changed and we are done without updating the entity. Otherwise (i.e., if one of the previous conditions is not satisfied), we write the entity to the store updating all files. Currently, we do not read declaration contents from the store. For a proof, the following files are created: proof__decl.xgz Gzipped XML file representing the proof of the formula . ... ... __refs.xml XML file representing the symbols referenced in the declaration: Writing a proof proceeds as explained for the declarations above. When a proof is read from the store, it is assumed that all the symbols in memory have already been updated in the store. The proof is returned with status "skeleton=yes" and the status "closed" as listed in the file. The proof's "trusted" value is set to "true" iff the symbols listed in the "refs" file are stored with the same time stamps as listed in the file. Replaying such a proof must not cause errors. The proof's "absolute" value is set to "true" iff the proof is "trusted" and "closed" and all formulas listed in the "refs" file have absolute proofs.

Constructor Summary

Store(java.io.File directory)
Create instance of store for denoted directory.

Method Summary

boolean	existsProof(FormulaSymbol symbol) Check whether store holds proof of formula.
boolean	hasChanged(Declaration decl) Signal whether declaration has changed compared to that in store.
boolean	hasChanged(java.util.HashMap dep, java.util.Collection referenced) Signal whether dependencies have changed compared to that in store.
static Declaration	readDeclaration(java.io.File file) Read declaration from file.
Proof	readProof(FormulaSymbol symbol) Read proof for formula from store.
static void	removeWhitespace(org.w3c.dom.Node node) Removes all text nodes that only contain whitespace from DOM tree.
static Declaration	toDeclaration(org.w3c.dom.Node node) Convert DOM node to declaration.
static Expression	toExpression(org.w3c.dom.Node node) Convert DOM node to expression.
static Identifier	toIdentifier(org.w3c.dom.Node node) Convert DOM node to identifier.
static Type	toType(org.w3c.dom.Node node) Convert DOM node to type.
boolean	write(Declaration decl, java.util.Collection referenced) Write value declaration to store.
boolean	write(Proof proof) Write proof to store updating the dependencies file.
boolean	writeDep(java.io.File file, java.util.Collection referenced) Write dependencies to file.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Store

public Store(java.io.File directory)

Create instance of store for denoted directory.

Parameters:

directory - for storing the declared objects

Method Detail

write

public boolean write(Proof proof)

Write proof to store updating the dependencies file.

Parameters:

proof - the proof

Returns:

true iff no problem occured in storing

existsProof

public boolean existsProof(FormulaSymbol symbol)

Check whether store holds proof of formula.

Parameters:

symbol - a formula symbol.

Returns:

true iff store holds a proof of the formula.

readProof

public Proof readProof(FormulaSymbol symbol)

Read proof for formula from store.

Parameters:

symbol - a formula symbol.

Returns:

the proof of the formula (or null, if an error occurred).

write

public boolean write(Declaration decl,
                     java.util.Collection referenced)

Write value declaration to store.

Parameters:

decl - the declaration

referenced - the symbols referenced in the definition of the symbol

Returns:

true iff no problem occured in storing

hasChanged

public boolean hasChanged(Declaration decl)

Signal whether declaration has changed compared to that in store.

Parameters:

decl - a declaration

Returns:

true iff store declaration is different from current one

hasChanged

public boolean hasChanged(java.util.HashMap dep,
                          java.util.Collection referenced)

Signal whether dependencies have changed compared to that in store.

Parameters:

dep - a dependencies map.

referenced - collection of symbols of referenced values

Returns:

true iff stored dependencies different from current one

writeDep

public boolean writeDep(java.io.File file,
                        java.util.Collection referenced)

Write dependencies to file.

Parameters:

file - the file to write to.

referenced - collection of symbols of referenced values

Returns:

true iff no problem occured in writing.

readDeclaration

public static Declaration readDeclaration(java.io.File file)

Read declaration from file.

Parameters:

file - path to a file holding the declaration.

Returns:

the declaration (null, if an error occured).

toExpression

public static Expression toExpression(org.w3c.dom.Node node)

Convert DOM node to expression.

Parameters:

node - the DOM representation of the expression.

Returns:

the expression (null, if an error occured).

toType

public static Type toType(org.w3c.dom.Node node)

Convert DOM node to type.

Parameters:

node - the DOM representation of the type.

Returns:

the type (null, if an error occured).

toIdentifier

public static Identifier toIdentifier(org.w3c.dom.Node node)

Convert DOM node to identifier.

Parameters:

node - the DOM representation of the identifier.

Returns:

the type (null, if an error occured).

toDeclaration

public static Declaration toDeclaration(org.w3c.dom.Node node)

Convert DOM node to declaration.

Parameters:

node - the DOM representation of the declaration.

Returns:

the declaration (null, if an error occured).

removeWhitespace

public static void removeWhitespace(org.w3c.dom.Node node)

Removes all text nodes that only contain whitespace from DOM tree.

Parameters:

node - the root of the tree that is to be cleaned from whitespace.