Rule-based Web site verification

The Web specification language

• A Web specification is a triple (R,IN,IM), where R, IN, and IM are a finite set of rules. The set R contains the definition of some auxiliary functions which the user would like to provide, such as string processing, arithmetic, boolean operators, etc. R is formalized as a term rewriting system, which is handled by standard rewriting klo91. The rewriting mechanism executes function calls by simply reducing them to their irreducible form (that is, a term that cannot be rewritten further). The set IN describes constraints for detecting erroneous Web pages (correctNess rules). A correctness rule has the following syntax:

  l -> error |C

  where l is a term, error is a reserved constant, and C is a (possibly empty) finite sequence containing

      - membership tests of the form X \in rexp w.r.t. a given regular language rexp;
      - equations/inequalities over terms.

  When C is empty, we simply write l -> error. Informally, the meaning of a correctness rule l -> error |C is the following. Whenever (i) a "piece" of a given Web page can be "recognized" to be an instance of l, and (ii) the corresponding instantiated condition holds, then Web page is marked as an incorrect page. The third set of rules IM specifes some properties for discovering incomplete/missing Web pages ( coMpleteness rules). A completeness rule is defined as

  l -> r {q}

  where l and r are terms and q can be A or E. Completeness rules of a Web specification formalize the requirement that some information must be included in all or some pages of the Web site. We use attributes {A} and {E} to distinguish "universal" from "existential" rules, as explained below. Right-hand sides r of completeness rules can contain functions, which are defined in R. In addiction, some symbols in the right-hand sides of the rules may be marked by means of the symbol #. Marking information of a given rule r is used to select the subset of the Web site in order to check the condition formalized by r. Intuitively, the interpretation of a universal rule l -> r {A} (respectively, an existential rule l -> r {E}) w.r.t. a Web site \Website is as follows: if (an instance of) l is "recognized" in the Web Site, (an instance of) the irreducible form of r must also be "recognized" in all (respectively, some) of the Web pages that embed (an instance of) the marked structure of r. Let R be a TRS, we define X ++Y , which concatenates two strings; we also define X+Y, which sums two natural numbers. Let (R,IN,IM) be a Web specification where IN and IM are defined as follows:

  member(name(X),surname(Y)) -> #hpage(fullname(X++Y)),status)  {E} 
  hpage(status(professor)) -> #hpage(#status(#professor),teaching)) {A} 
  project(grant1(X),grant2(Y),total(Z)) -> error X+Y <> Z
  

  This Web specification models some required properties for a Web site of a research group. The first rule formalizes the following property: if there is a Web page containing a member list, then for each member, a home page should exist which contains (at least) the full name and the status of this member. The full name is computed by applying the function ++ to the name and the surname of the member. The marking information establishes that the property must be checked only on home pages (i.e., pages containing the tag "hpage"). The second rule states that, whenever a home page of a professor is recognized, that page must also include some teaching information. The rule is universal since it must hold for each professor home page (i.e., all the Web pages embedding the marked structure home(status(professor)). The third rule states that, for each research project, the total project budget must be equal to the sum of the funds, which have been granted for the first and the second research periods. The membership tests in the conditions ensure that the values assigned to the variables are natural numbers. Diagnoses are carried out by running Web specifications on Web sites. The operational mechanism is based on a novel, flexible matching technique ABF06 that is able to "recognize" the partial structure of a term (Web template) within another and select it by computing homeomorphic embeddings of Web patterns within Web documents.