[ 
https://issues.apache.org/jira/browse/CALCITE-1977?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=16159489#comment-16159489
 ] 

Michael Mior commented on CALCITE-1977:
---------------------------------------

Not written in Java, but Rosette (Racket) and Coq (Haskell). The easiest 
approach would probably be to just shell out to the tool. Also worth noting 
that it doesn't prove that rewrite rules are valid, but only that two queries 
are equivalent. So we could check that a *particular* rewrite is valid, but it 
doesn't necessarily mean that the rule is always correct.

> Use Cosette to check whether planner rules are valid
> ----------------------------------------------------
>
>                 Key: CALCITE-1977
>                 URL: https://issues.apache.org/jira/browse/CALCITE-1977
>             Project: Calcite
>          Issue Type: Bug
>            Reporter: Julian Hyde
>            Assignee: Julian Hyde
>
> Use [Cosette|http://cosette.cs.washington.edu/], an automated SQL solver from 
> University of Washington, to check whether planner rules are valid.
> I don't know whether Cosette is written in Java, so the simplest approach 
> might be to instrument the planner to generate a script. Suppose 
> {{FilterProjectTransposeRule}} has just fired successfully. Then 
> {{RelOptRuleCall#transformTo}} would generate the line
> {code}
>   assertEquivalent(
>     "select * from (select empno from emp) where empno > 10",
>     "select empno from (select * from emp where empno > 10)")
> {code}
> (Those SQL statements are the result of converting the before and after 
> {{RelNode}} instances to SQL.)
> We could run the Calcite test suite to produce a large script with probably 
> thousands of those statements. Then the Cosette researchers can take that 
> script and run it through Cosette (using whatever language they develop in). 
> It would find bugs in Cosette (at first mostly deficiencies in Cosette's SQL 
> parser, I fear) but also would find bugs in Calcite if the transformation is 
> not valid. (Not too many, I hope!)



--
This message was sent by Atlassian JIRA
(v6.4.14#64029)

Reply via email to