Comments ...

[Harald Ruess]

Hi all,

Here are some initial and, admittedly, rather unpolished remarks 
on some recent discussions about the proposed combination 
benchmark library.

1. No sort system! Our aim here is to exchange benchmark
 examples, not to do language design
 I do not want to start yet another discussion on the relative benefits 
 of sorted vs. unsorted. However, it seems obvious to me that we don't 
 want to rule out backend proof procedures for languages such as, say, Lisp.

2. No explicit language for syntactic restrictions.
 It is ok, however, to have a 'comment' (see item 6.) that 
 a benchmark falls into a certain fragment. If we start having these
 restrictions, we will soon have almost as many so-called "logics" as
 benchmarks. In one of the previous mails, Pratt's difference logic
 was mentioned as an example. This is just a fragment of
 linear arithmetic which happens to have a well-behaved decision
 procedure. It is interesting in that about 90% of proof obligations
 in typical software verification fall into this fragment, so a good
 verification tool has to support this fragment efficiently---but the 
 remaining 10% have to be dealt with, too.  Or do we really want to
 explicitly support benchmarks for impoverished systems such as, say, 
 timed automata?

3. There should be a base logic, which includes a reasonable number
  of different theories.  My suggestion is to have a rather small
  number of theories in this base logic, namely conjunctions of
  literals built from
      - Rational (and maybe integer) linear arithmetic (with inequalities)
      - Equality over uninterpreted functions
      - Propositional constants true and false 
  The number of theories in the core logic should be >1,
  since our main emphasis here is to promote combination procedures
  (see also 2.). 

4. The base logic already includes lets (they are useful and
   harmless), but no propositional connectives or explicit quantification.  
   This base logic can be extended
      - horizontally, by specifying more theories
      - vertically, by introducing propositional connectives and 
        first-order quantification.
   Another extension could be along the dimension of various type systems
   (cmp 1.), but then the benchmark infrastructure should support 
   translations (tools) into an untyped fragment. Besides that we should,
   at least initially, avoid any deeper issues about structuring descriptions
   of theories.

5. No need for declaring function symbols, since arity is
   deduced from first occurrence as suggested earlier. Mechanism 
   for declaring function symbols should allow for infinite families of
   function symbols (is indexing with respect to a Cartesian
   product of naturals enough?). There might even be the 
   possibility to declare a function symbol to be AC etc
   (in which case we should possibly allow for arbitrary
   n-ary application).

6. Dinstinction between machine-readable part of a benchmark
   example and the organizational part (spec of theory etc.).

7. Include constructs for specifying expected
  return values. Should we also have standard formats for proof
  objects? Probably not in the initial phase.

8. Altogether, a small example in the benchmark could look like follows 
  
     (:benchmark "0"            ; admin stuff such as provider, date etc may go in here
      :theory (:union LA U)     ; the core logic of linear arithmetic LA and uninterpreted
      (:proposition             ; function symbols U
         (:turnstyle
           (:conjunction
              (:equal z (:app f (:minus x y)))
              (:equal x (:plus z y)))
           (:diseq (:minus y)
                   (:minus (:minus x (:app f (:app f z))))))
         :value :unsat)
      (:proposition
             ...))

   Semantics is obvious.  I do not really care about the "concrete" form of the 
   chosen abstract syntax as long as it is easily parsable (in particular, no XML).


Cheers,

Harald