The goal of PUBS is to automatically obtain closed form upper bounds for Cost Equation Systems. For this, PUBS computs upper bounds for the cost relation indicated as the Entry, plus for all other cost relations on which such entry depends.

In the output, not only we show the upper bound obtained but we also show the results of the intermediate steps performed, which involve computing ranking functions and loop invariants. In order to use the solver, the steps to follow are:

Step 1: Provide a Cost Equation System.

• by either typing it in the text-area, or
• uploading a file.

Step 2: Provide an Entry. There are three possibilities here:

• manually typing it in the Entry box,
• if the CES already contains entries, type in a number in the IEntry # box.
• if both boxes are left blank the system will assume that the entry coincides with the first equation as initial entry, with no initial constraint.

Step 3: click on the Solve button.

Syntax

Equation::= eq(Head, CostExpression, ListOfCalls, ListOfSizeRelations).

Head::= Name | Name(Arguments) 

Arguments ::= Variable | Variable,Arguments

ListOfCalls ::= [] |[Head|ListOfCalls]

ListOfSizeRelations ::= [] | [SizeRelation|ListOfSizeRelations]

SizeRelation ::= Variable Oper LinearExpression

Oper ::=  >= | <= | =

LinearExpression ::= RationalNumber * Variable | RationalNumber * Variable + LinearExpression

CostExpression :: = PositiveRationalNumber                           | 
                    nat(LinearExpression)                            | 
                    CostExpression * CostExpression                  |
                    CostExpression + CostExpression                  |
                    pow(PositiveRationalNumber,CostExpression)       |
                    log(NaturalNumber,CostExpression)                |
                    NaturalNumber^CostExpression                     |
                    max(ListOfCostExpressions)                       

ListOfCostExpressions :: = [] | [CostExpression|ListOfCostExpressions]



* A "Name" can be either a sequence of characters between quotes or any
  sequence of consecutive characters (only letters and numbers) 
  beginning with a lower letter. Examples of valid names are:
 
       'function factorial'
       factorial
       factorial1

  Examples of invalid names are:

       Factorial
       1factorial
       function factorial


* Variables follows Prolog syntax, i.e., are sequences of characters
  (letters or numbers) beginning with a capital letter. Examples of
  valid variables are:

      X
      Variable1
    

* A PositiveRationalNumber has the form NaturalNumber/NaturalNumber

* RationalNumber is either a PositiveRationalNumber or -PositiveRationalNumber