# Test whether a schema mentions the predicates used in this data # This involves searching in files for statements being present or absent. @prefix rdf: . @prefix s: . # @prefix dpo: . @prefix log: . @prefix os: . @prefix : . # Local stuff @prefix val: . # Local stuff # Usage: to validate myfile.n3, # cwm validate.n3 -think -purge --with myfile.n3 # # # Output should not incldue any error messages. # (look for "ERROR" in caps) # this log:forAll :c, :d, :o, :p, :r, :s, :S, :s1, :x, :y, :F, :G, :H. # Some internal terms we will be using in this document: # These are declared here because older versions of the validator # checked for the. Later versions assume local (<#>) variables are # used consistently. :usedAsPropertyIn a rdf:Property; s:comment "This term is used as a Property in the given document."; a log:Chaff. # Internal use only, may be purged. :within a rdf:Property; s:comment "relationship between a subforumula and the document it was found in"; a log:Chaff. # Internal use only, may be purged. :targetDocument a s:Class; s:comment "Documents which this run is checking for schema validity"; a log:Chaff. # Internal use only, may be purged. #:propertySchema a rdf:Property; # s:comment "The schema for a Property is the document which defines it.". :ERROR_NO_SCHEMA_OR_NOT_DECLARED a rdf:Property; s:comment """The document used this as a predicate and there is no schema which declares it as a Property""". :ERROR_PROPERTY_NOT_DECLARED a rdf:Property. ##################################################################################### # Target formulae are the top level formula we are pointed at, # and any subformulae. # (The command line arguments we get are those after cwm's --with ) { :d log:uri "1"!os:argv!os:baseAbsolute } log:implies { :d a :targetDocument }. { :d a :targetDocument. :d log:semantics :F } log:implies { :F :within :d }. # Define subforumulae which are within the target documents: { :d a :targetDocument. :F :within :d. :F log:includes { :s :p :o}. :s log:rawType log:Formula } log:implies { :s :within :d } . { :d a :targetDocument. :F :within :d. :F log:includes { :s :p :o}. :o log:rawType log:Formula } log:implies { :o :within :d } . # Anything used as a predicate in any target formula should be checked. # We don't bother bout the pseudoproperties log:forSome and log:forAll. { :d a :targetDocument. :F :within :d. :F log:includes { :s :p :o}. :p log:rawType log:Other. # Ignore lists :p log:notEqualTo log:forSome, log:forAll. :p log:racine :r } log:implies { :p :usedAsPropertyIn :d; :usedIn :d. :d :usesRacine :r } . { :d a :targetDocument. :F :within :d. :F log:includes { :s a :c}. :c log:racine :r } log:implies { :c :usedAsClassIn :d; :usedIn :d. :d :usesRacine :r } . # Let's see what happens when we dereference a predicate or type: # # We could dereference the predicate itself, but to simplfy life # we find the racine (the thing without the "#") whcih is what we would # get anyway. And we can use the same rules for classes { :d a :targetDocument; :usesRacine :r. :r log:semanticsOrError :x. :x log:rawType log:Literal } log:implies { :d :ERROR_IN_NAMESPACE_ACCESS_FOR :r. :r :NAMESPACE_ACCESS_ERROR :x }. { :d a :targetDocument; :usesRacine :r. :r log:semanticsOrError :x. :x log:rawType log:Formula } log:implies { :r :semanticsOK :x }. # The RDFS spec implies the following algorithm for the definitive schema corresponding # to a Property :p. (From Ralph Swick, whiteboard conversation) # Maybe we should simplify it to the schema being the result of dereferencing the Property? # I think the counterexample is the dublin core, but it may not work anyway. # Actually, the dublic core uses a redirect!!! We need to be aware of the # existence of redirects like that @@ { :d a :targetDocument. :p :usedIn :d; log:racine :r. :r :semanticsOK [log:includes { :p s:isDefinedBy :s }]. } log:implies { :p :schema :s. :d :documentSchema :s. }. # The normal case is with no redirection: { :d a :targetDocument. :p :usedIn :d; log:racine :r. :r :semanticsOK [log:notIncludes { :p s:isDefinedBy [] }]. } log:implies { :p :schema :r. :d :documentSchema :r. }. # The schema semantics we get from resolving the schema: { :d a :targetDocument; :documentSchema :s. :s log:semanticsOrError :x. :x log:rawType log:Literal } log:implies { :d :ERROR_IN_SCHEMA_ACCESS_FOR :s. :s :SCHEMA_ACCESS_ERROR :x }. { :d a :targetDocument; :documentSchema :s. :s log:semanticsOrError :x. :x log:rawType log:Formula } log:implies {:s :semanticsOK :x}. # s above maybe the same as :r above that but it doesn't matter. # We *actually* need the formula the schema parses to, augmented by its axioms: { :d :documentSchema :s. :s :semanticsOK :F. (:F [is log:semantics of ] [is log:semantics of ]) log:conjunction [log:conclusion :G]. } log:implies { :s :augmented :G }. # We don't insist that the schema *directly* defined properties and # classes as such. We take as given the axioms of rdfs. # Here, we consider an augmented schema which is the deductive closure # of the original schema and the axioms: # It is an error, we say, for something to be used as a Property but # not im plicitly or explicitly declared as such in the schema, that is, # not explicitly declared as such in the augmented schema. # # (That is, except for local identifiers, which we assume to be used correctly. # Note this looseness is a choice: we could require local declarations, # to follow a more traditionally careful software engineering style.) { :d a :targetDocument. :p :usedAsPropertyIn :d; log:racine :r. :r log:notEqualTo :d. # Not local :p :schema [:augmented [log:notIncludes { :p a rdf:Property }]]. } log:implies { :d :ERROR_PREDICATE_NOT_DECLARED_AS_PROPERTY :p }. { :d a :targetDocument. :c :usedAsClassIn :d; log:racine [log:notEqualTo :d]. # Not local :c :schema [:augmented [log:notIncludes { :c a s:Class }]]. } log:implies { :d :ERROR_TYPE_NOT_DECLARED_AS_CLASS :c }. # (b)when the document is combined with the above, no contradiction # can be found from anything being (eg) member of disjoint sets. # { :d :documentSchema :s; log:semantics :F. :s :augmented :G. (:F :G) log:conjunction [has log:conclusion [log:includes {[] :ERROR []}]] } log:implies { :d :ERROR_INCONSISTENCY_W_R_T_SCHEMA :s }. ################################################################### Clean up {:d a :targetDocument. :F :within :d } log:implies { :F a log:Chaff }. # Clear our formulae log:Chaff is rdf:type of rdf:type, # Seriously ... s:comment, :documentSchema, :usesRacine, :schema, :usedAsClassIn, :usedIn, log:forAll, log:implies, # Clear out rules on -purge :within, :schemaFormula, :augmented, :semanticsOK, :usedAsPropertyIn. #ends