Store

java.lang.Object
- fmrisc.ProofNavigator.Communication.Store

```
public final class Store
extends java.lang.Object
```
Persistent store of declarations and proofs. For a declaration NAME of KIND (where KIND in {type,value,formula}) the following files are created: KIND_NAME_decl.xgz Gzipped XML file holding the OMDoc representation of the declaration. (Since the declaration is actually not needed, we don't generate it any more). KIND_NAME_hash.txt (not for proofs) A single text line with a hash value for the representation (a non-negative integer number in decimal representation). KIND_NAME_time.txt A single text line with a time stamp (a non-negative integer number in decimal representation). KIND_NAME_refs.xml XML file representing the symbols referenced in the declaration: fmrisc:refs fmrisc:KIND time="timestampvalue" NAME /fmrisc:KIND ... /fmrisc:refs 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_NAME_decl.xgz Gzipped XML file representing the proof of the formula NAME. fmrisc:proof name="formulaname" closed="true|false" fmrisc:state fmrisc:command /fmrisc:command fmrisc:state.../fmrisc:state ... /fmrisc:state /fmrisc:proof KIND_NAME_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.

Field Summary

Fields
Modifier and Type Field and Description

static long HASH_DEFAULT

static long STAMP_DEFAULT

Fields
Modifier and Type	Field and Description
`static long`	`HASH_DEFAULT`
`static long`	`STAMP_DEFAULT`

Constructor Summary

Constructors
Constructor and Description

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

Constructors
Constructor and Description
`Store(java.io.File directory)` Create instance of store for denoted directory.

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`boolean`	`existsProof(FormulaSymbol symbol)` Check whether store holds proof of formula.
`boolean`	`existsProof(java.lang.String name)` Check whether store holds proof of formula.
`boolean`	`hasChanged(Declaration decl)` Signal whether declaration has 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<Symbol> referenced)` Write declaration to store.
`boolean`	`write(Proof proof)` Write proof to store updating the dependencies file.

Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - HASH_DEFAULT
```
public static final long HASH_DEFAULT
```
    See Also:
    
    Constant Field Values
  - STAMP_DEFAULT
```
public static final long STAMP_DEFAULT
```
    See Also:
    
    Constant Field Values
- 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(java.lang.String name)
```
    Check whether store holds proof of formula.
    
    Parameters:
    
    name - the name of a formula.
    
    Returns:
    
    true iff store holds a proof of the formula.
  - 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<Symbol> referenced)
```
    Write 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
  - 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.

Class Store

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

HASH_DEFAULT

STAMP_DEFAULT

Constructor Detail

Store

Method Detail

write

existsProof

existsProof

readProof

write

hasChanged

readDeclaration

toExpression

toType

toIdentifier

toDeclaration

removeWhitespace