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.
- 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.
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