04-abstracting.html

<!DOCTYPE html>
<html lang="en">
<head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1.0">
    <meta name="generator" content="rustdoc">
    <title>Language-Integrated Verification</title>

    <link href="./css/bootstrap.css" rel="stylesheet">
    <link href="./css/bootstrap-theme.css" rel="stylesheet">
    <link rel="stylesheet" type="text/css" href="./css/rust-book-slides.css">
    <link rel="stylesheet" type="text/css" href="./css/editor-slides.css">
    <link rel="stylesheet" type="text/css" href="./css/code-format.css">
    <link rel="stylesheet" type="text/css" href="./css/slideshow.css">
    <style>
      body {
        text-align: center;
      }
      .mybreak {
        line-height: 1em;
      }
      table {
        margin-left: 150px;
        margin-right: auto;
      }
    </style>

    <!-- JQUERY MOBILE -->

    <!-- Include jQuery Mobile stylesheets -->

    <!-- Include the jQuery library -->
     <!-- <script src="http://code.jquery.com/jquery-1.11.3.min.js"></script> -->
     <script src="./js/jquery/jquery-1.11.3.min.js"></script>
     <script src="./js/jquery/init-mobile.js"></script>

     <!-- Include the jQuery Mobile library -->
     <!-- <script src="http://code.jquery.com/mobile/1.4.5/jquery.mobile-1.4.5.min.js"></script> -->
     <script src="./js/jquery/jquery.mobile-1.4.5.min.js"></script>

<!-- JQUERY LOCAL

<script type="text/javascript" src="./js/jquery/jquery-2.0.3.min.js"></script>

-->


<script type="text/javascript" src="./js/angular/angular.js"></script>
<script type="text/javascript" src="./js/bootstrap/bootstrap.js"></script>

<script type="text/x-mathjax-config">
MathJax.Hub.Config({
  TeX: {
    extensions: ["color.js"],
    Macros: {
      True: "\\mathit{True}",
      RR:   "{\\bf R}",
      Int:  "\\mathtt{Int}",
      Nat:  "\\mathtt{Nat}",
      Zero: "\\mathtt{Zero}",
      foo:   ["{\\bf Jhala FOO #1}", 1],
      kvar:  ["{\\color[rgb]{1,0,0}{K_{#1}({#2})}}", 2],
      bindx: ["{{#1}\\!:\\!{#2}}", 2],
      reft:  ["\\{\\bindx{#1}{#2} \\mid {#3}\\}", 3],
      ereft: ["\\bindx{#1}{\\{#2 \\mid #3\\}}", 3],
      reftx: ["\\{{#1}\\mid{#2}\\}", 2],
      inferrule: ["\\frac{#2}{#3}\\;{#1}", 3]
  }
  }
});
</script>

<!-- GITHUB
<script src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script>
-->

<!-- LOCAL -->
<script src="js/MathJax-2.6.0/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script>


</head>

<body class="rustdoc" data-spy="scroll" data-target=".bs-docs-sidebar" ng-app="liquidDemo" ng-controller="LiquidDemoCtrl">


  <div id="nav">

        <button class="btn btn-xs btn-link actbutton firstbutton" type="button" style="font-size:15px; color:black; z-index:1">
          <span class="glyphicon glyphicon-backward"></span>
        </button>

        <button class="btn btn-xs btn-link actbutton prevbutton" type="button" style="font-size:15px; color:black;  z-index:1">
          <span class="glyphicon glyphicon-chevron-left"></span>
        </button>

        <button id="toggle-nav" class="toggle-nav">
          <span class="sr-only">Toggle navigation</span>
          <span class="bar"></span>
          <span class="bar"></span>
        </button>

        <button class="btn btn-xs btn-link actbutton nextbutton" type="button" style="font-size:15px; color:black; z-index:1">
          <span class="glyphicon glyphicon-chevron-right"></span>
        </button>

        <button class="btn btn-xs btn-link actbutton lastbutton" type="button" style="font-size:15px; color:black; z-index:1">
          <span class="glyphicon glyphicon-forward"></span>
        </button>

  </div>

<div id='toc' class='mobile-hidden'>
<ul class='chapter'>
<li><a href='01-intro.html'><b>1.</b>Follow Along at This URL</a></li>
<ul class='section'>
<li><a href='01-intro.html#whats-this'><b>1.1.</b> Whats this?</a></li>
<li><a href='01-intro.html#the-first-bug'><b>1.2.</b> The First <em>Bug</em></a></li>
<li><a href='01-intro.html#fast-forward-to-present-day'><b>1.3.</b> Fast forward to Present Day</a></li>
<li><a href='01-intro.html#fast-forward-to-present-day-1'><b>1.4.</b> Fast forward to Present Day</a></li>
<li><a href='01-intro.html#fast-forward-to-present-day-2'><b>1.5.</b> Fast forward to Present Day</a></li>
<li><a href='01-intro.html#programming-languages-research'><b>1.6.</b> Programming Languages Research</a></li>
<li><a href='01-intro.html#modern-languages'><b>1.7.</b> Modern Languages</a></li>
<li><a href='01-intro.html#modern-languages-1'><b>1.8.</b> Modern Languages</a></li>
<li><a href='01-intro.html#modern-languages-2'><b>1.9.</b> Modern Languages</a></li>
<li><a href='01-intro.html#modern-languages-3'><b>1.10.</b> Modern Languages?</a></li>
<li><a href='01-intro.html#well-typed-programs-can-go-very-wrong'><b>1.11.</b> Well-typed programs can go very wrong!</a></li>
<li><a href='01-intro.html#well-typed-programs-can-go-very-wrong-1'><b>1.12.</b> Well-typed programs can go very wrong!</a></li>
<li><a href='01-intro.html#well-typed-programs-can-go-very-wrong-2'><b>1.13.</b> Well-typed programs can go very wrong!</a></li>
<li><a href='01-intro.html#goal-language-integrated-verification'><b>1.14.</b> Goal: Language-Integrated Verification</a></li>
<li><a href='01-intro.html#goal-language-integrated-verification-1'><b>1.15.</b> Goal: Language-Integrated Verification</a></li>
<li><a href='01-intro.html#outline'><b>1.16.</b> Outline</a></li>
<li><a href='01-intro.html#outline-1'><b>1.17.</b> Outline</a></li>
<li><a href='01-intro.html#outline-2'><b>1.18.</b> Outline</a></li>
<li><a href='01-intro.html#outline-3'><b>1.19.</b> Outline</a></li>
<li><a href='01-intro.html#outline-4'><b>1.20.</b> Outline</a></li>
<li><a href='01-intro.html#outline-5'><b>1.21.</b> Outline</a></li>
</ul>
<li><a href='02-refinements.html'><b>2.</b>Simple Refinement Types</a></li>
<ul class='section'>
<li><a href='02-refinements.html#types'><b>2.1.</b> Types</a></li>
<li><a href='02-refinements.html#predicates'><b>2.2.</b> Predicates</a></li>
<li><a href='02-refinements.html#predicates-1'><b>2.3.</b> Predicates</a></li>
<li><a href='02-refinements.html#predicates-2'><b>2.4.</b> Predicates</a></li>
<li><a href='02-refinements.html#predicates-3'><b>2.5.</b> Predicates</a></li>
<li><a href='02-refinements.html#predicates-4'><b>2.6.</b> Predicates</a></li>
<li><a href='02-refinements.html#example-singletons'><b>2.7.</b> Example: Singletons</a></li>
<li><a href='02-refinements.html#example-natural-numbers'><b>2.8.</b> Example: Natural Numbers</a></li>
<li><a href='02-refinements.html#a-term-can-have-many-types'><b>2.9.</b> A Term Can Have <em>Many</em> Types</a></li>
<li><a href='02-refinements.html#predicate-subtyping-nuprl-pvs'><b>2.10.</b> 1. Predicate Subtyping <a href="http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf">[NUPRL, PVS]</a></a></li>
<li><a href='02-refinements.html#predicate-subtyping-nuprl-pvs-1'><b>2.11.</b> 1. Predicate Subtyping <a href="http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf">[NUPRL, PVS]</a></a></li>
<li><a href='02-refinements.html#predicate-subtyping-nuprl-pvs-2'><b>2.12.</b> 1. Predicate Subtyping <a href="http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf">[NUPRL, PVS]</a></a></li>
<li><a href='02-refinements.html#example-natural-numbers-1'><b>2.13.</b> Example: Natural Numbers</a></li>
<li><a href='02-refinements.html#example-natural-numbers-2'><b>2.14.</b> Example: Natural Numbers</a></li>
<li><a href='02-refinements.html#typing-applications-function-calls'><b>2.15.</b> 2. Typing Applications (Function Calls)</a></li>
<li><a href='02-refinements.html#typing-applications-function-calls-1'><b>2.16.</b> 2. Typing Applications (Function Calls)</a></li>
<li><a href='02-refinements.html#typing-applications-function-calls-2'><b>2.17.</b> 2. Typing Applications (Function Calls)</a></li>
<li><a href='02-refinements.html#typing-applications-function-calls-3'><b>2.18.</b> 2. Typing Applications (Function Calls)</a></li>
<li><a href='02-refinements.html#recap-refinement-types-101'><b>2.19.</b> Recap: Refinement Types 101</a></li>
<li><a href='02-refinements.html#recap-refinement-types-101-1'><b>2.20.</b> Recap: Refinement Types 101</a></li>
<li><a href='02-refinements.html#recap-refinement-types-101-2'><b>2.21.</b> Recap: Refinement Types 101</a></li>
<li><a href='02-refinements.html#outline'><b>2.22.</b> Outline</a></li>
<li><a href='02-refinements.html#outline-1'><b>2.23.</b> Outline</a></li>
</ul>
<li><a href='03-examples.html'><b>3.</b>Refinement Types by Example</a></li>
<ul class='section'>
<li><a href='03-examples.html#refinement-types-by-example-1'><b>3.1.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#refinement-types-by-example-2'><b>3.2.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#refinement-types-by-example-3'><b>3.3.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#specifications-pre-conditions'><b>3.4.</b> Specifications: Pre-Conditions</a></li>
<li><a href='03-examples.html#specifications-post-conditions'><b>3.5.</b> Specifications: Post-Conditions</a></li>
<li><a href='03-examples.html#refinement-types-by-example-4'><b>3.6.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#verification-vector-sum'><b>3.7.</b> Verification: Vector Sum</a></li>
<li><a href='03-examples.html#verification-vector-sum-1'><b>3.8.</b> Verification: Vector Sum</a></li>
<li><a href='03-examples.html#verification-vector-sum-2'><b>3.9.</b> Verification: Vector Sum</a></li>
<li><a href='03-examples.html#refinement-types-by-example-5'><b>3.10.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#inference'><b>3.11.</b> Inference</a></li>
<li><a href='03-examples.html#inference-vector-sum'><b>3.12.</b> Inference: Vector Sum</a></li>
<li><a href='03-examples.html#inference-vector-sum-1'><b>3.13.</b> Inference: Vector Sum</a></li>
<li><a href='03-examples.html#inference-vector-sum-2'><b>3.14.</b> Inference: Vector Sum</a></li>
<li><a href='03-examples.html#inference-vector-sum-3'><b>3.15.</b> Inference: Vector Sum</a></li>
<li><a href='03-examples.html#inference-vector-sum-4'><b>3.16.</b> Inference: Vector Sum</a></li>
<li><a href='03-examples.html#inference-vector-sum-5'><b>3.17.</b> Inference: Vector Sum</a></li>
<li><a href='03-examples.html#refinement-types-by-example-6'><b>3.18.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#collections-higher-order-functions'><b>3.19.</b> Collections &amp; Higher-Order Functions</a></li>
<li><a href='03-examples.html#collections-higher-order-functions-1'><b>3.20.</b> Collections &amp; Higher-Order Functions</a></li>
<li><a href='03-examples.html#collections-higher-order-functions-2'><b>3.21.</b> Collections &amp; Higher-Order Functions</a></li>
<li><a href='03-examples.html#collections-higher-order-functions-3'><b>3.22.</b> Collections &amp; Higher-Order Functions</a></li>
<li><a href='03-examples.html#refinement-types-by-example-7'><b>3.23.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#example-list-average'><b>3.24.</b> Example: List <code>average</code></a></li>
<li><a href='03-examples.html#refinements-for-datatypes'><b>3.25.</b> Refinements for Datatypes</a></li>
<li><a href='03-examples.html#measures-yield-refined-constructors'><b>3.26.</b> Measures Yield Refined Constructors</a></li>
<li><a href='03-examples.html#example-map-over-lists'><b>3.27.</b> Example: <code>map</code> over Lists</a></li>
<li><a href='03-examples.html#refinements-for-datatypes-1'><b>3.28.</b> Refinements for Datatypes</a></li>
<li><a href='03-examples.html#refinements-for-datatypes-2'><b>3.29.</b> Refinements for Datatypes</a></li>
<li><a href='03-examples.html#refinements-for-datatypes-3'><b>3.30.</b> Refinements for Datatypes</a></li>
<li><a href='03-examples.html#refinement-types-by-example-8'><b>3.31.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#outline'><b>3.32.</b> Outline</a></li>
<li><a href='03-examples.html#outline-1'><b>3.33.</b> Outline</a></li>
</ul>
<li><a href='04-abstracting.html'><b>4.</b>Invariants In Constructors</a></li>
<ul class='section'>
<li><a href='04-abstracting.html#invariants-in-constructors-1'><b>4.1.</b> Invariants In Constructors</a></li>
<li><a href='04-abstracting.html#invariants-in-constructors-2'><b>4.2.</b> Invariants In Constructors</a></li>
<li><a href='04-abstracting.html#invariants-in-constructors-3'><b>4.3.</b> Invariants In Constructors</a></li>
<li><a href='04-abstracting.html#abstracting-refinements'><b>4.4.</b> Abstracting Refinements</a></li>
<li><a href='04-abstracting.html#abstracting-refinements-1'><b>4.5.</b> Abstracting Refinements</a></li>
<li><a href='04-abstracting.html#abstracting-refinements-2'><b>4.6.</b> Abstracting Refinements</a></li>
<li><a href='04-abstracting.html#using-abstract-refinements'><b>4.7.</b> Using Abstract Refinements</a></li>
<li><a href='04-abstracting.html#recap'><b>4.8.</b> Recap</a></li>
<li><a href='04-abstracting.html#recap-1'><b>4.9.</b> Recap</a></li>
<li><a href='04-abstracting.html#bounded-refinements-induction-as-a-type'><b>4.10.</b> Bounded Refinements: Induction as a Type</a></li>
<li><a href='04-abstracting.html#bounded-refinements-induction-as-a-type-1'><b>4.11.</b> Bounded Refinements: Induction as a Type</a></li>
<li><a href='04-abstracting.html#bounded-refinements-induction-as-a-type-2'><b>4.12.</b> Bounded Refinements: Induction as a Type</a></li>
<li><a href='04-abstracting.html#bounded-refinements-induction-as-a-type-3'><b>4.13.</b> Bounded Refinements: Induction as a Type</a></li>
</ul>
<li><a href='04-termination.html'><b>5.</b>Avoiding Infinite Loops</a></li>
<ul class='section'>
<li><a href='04-termination.html#example-proving-termination-of-sum'><b>5.1.</b> Example: Proving Termination of <code>sum</code></a></li>
<li><a href='04-termination.html#proving-termination'><b>5.2.</b> Proving Termination</a></li>
<li><a href='04-termination.html#proving-termination-1'><b>5.3.</b> Proving Termination</a></li>
<li><a href='04-termination.html#proving-termination-2'><b>5.4.</b> Proving Termination</a></li>
<li><a href='04-termination.html#proving-termination-3'><b>5.5.</b> Proving Termination</a></li>
<li><a href='04-termination.html#example-proving-termination-of-sum-1'><b>5.6.</b> Example: Proving Termination of <code>sum</code></a></li>
<li><a href='04-termination.html#user-specified-termination-metrics'><b>5.7.</b> User Specified Termination Metrics</a></li>
<li><a href='04-termination.html#user-specified-termination-metrics-1'><b>5.8.</b> User Specified Termination Metrics</a></li>
<li><a href='04-termination.html#user-specified-termination-metrics-2'><b>5.9.</b> User Specified Termination Metrics</a></li>
<li><a href='04-termination.html#proving-termination-4'><b>5.10.</b> Proving Termination</a></li>
<li><a href='04-termination.html#lexicographic-termination'><b>5.11.</b> Lexicographic Termination</a></li>
<li><a href='04-termination.html#how-about-data-types'><b>5.12.</b> How About Data Types?</a></li>
<li><a href='04-termination.html#user-specified-metrics-on-data-types'><b>5.13.</b> User specified metrics on Data Types</a></li>
<li><a href='04-termination.html#termination-can-be-tricky'><b>5.14.</b> Termination Can be Tricky</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-1'><b>5.15.</b> Avoiding Infinite Loops</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-2'><b>5.16.</b> Avoiding Infinite Loops</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-3'><b>5.17.</b> Avoiding Infinite Loops</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-4'><b>5.18.</b> Avoiding Infinite Loops</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-is-easy-in-practice'><b>5.19.</b> Avoiding Infinite Loops is Easy (in Practice)</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-is-easy-in-practice-1'><b>5.20.</b> Avoiding Infinite Loops is Easy (in Practice)</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-is-easy-in-practice-2'><b>5.21.</b> Avoiding Infinite Loops is Easy (in Practice)</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-is-easy-in-practice-3'><b>5.22.</b> Avoiding Infinite Loops is Easy (in Practice)</a></li>
<li><a href='04-termination.html#outline'><b>5.23.</b> Outline</a></li>
<li><a href='04-termination.html#outline-1'><b>5.24.</b> Outline</a></li>
</ul>
<li><a href='05-reflection.html'><b>6.</b>Types as Theorems, Programs as Proofs</a></li>
<ul class='section'>
<li><a href='05-reflection.html#types-as-theorems'><b>6.1.</b> Types As Theorems</a></li>
<li><a href='05-reflection.html#types-as-theorems-example'><b>6.2.</b> Types as Theorems: Example</a></li>
<li><a href='05-reflection.html#programs-as-proofs-example'><b>6.3.</b> Programs As Proofs: Example</a></li>
<li><a href='05-reflection.html#types-as-theorems-1'><b>6.4.</b> Types As Theorems</a></li>
<li><a href='05-reflection.html#types-as-theorems-example-1'><b>6.5.</b> Types as Theorems: Example</a></li>
<li><a href='05-reflection.html#programs-as-proofs-example-1'><b>6.6.</b> Programs As Proofs: Example</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-1'><b>6.7.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#those-proofs-were-boring'><b>6.8.</b> Those Proofs were Boring</a></li>
<li><a href='05-reflection.html#those-proofs-were-boring-1'><b>6.9.</b> Those Proofs were Boring</a></li>
<li><a href='05-reflection.html#theorems-about-functions'><b>6.10.</b> Theorems about Functions</a></li>
<li><a href='05-reflection.html#refinement-reflection'><b>6.11.</b> Refinement Reflection</a></li>
<li><a href='05-reflection.html#reflect-function-into-output-type'><b>6.12.</b> Reflect Function into Output Type</a></li>
<li><a href='05-reflection.html#reflect-function-into-output-type-1'><b>6.13.</b> Reflect Function into Output Type</a></li>
<li><a href='05-reflection.html#reflection-at-result-type'><b>6.14.</b> Reflection at Result Type</a></li>
<li><a href='05-reflection.html#structuring-proofs-as-calculations'><b>6.15.</b> Structuring Proofs as Calculations</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-2'><b>6.16.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#reusing-proofs-functions-as-lemmas'><b>6.17.</b> Reusing Proofs: Functions as Lemmas</a></li>
<li><a href='05-reflection.html#reusing-proofs-functions-as-lemmas-1'><b>6.18.</b> Reusing Proofs: Functions as Lemmas</a></li>
<li><a href='05-reflection.html#reusing-proofs-functions-as-lemmas-2'><b>6.19.</b> Reusing Proofs: Functions as Lemmas</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-3'><b>6.20.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-4'><b>6.21.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#proof-by-logical-evaluation'><b>6.22.</b> Proof by Logical Evaluation</a></li>
<li><a href='05-reflection.html#proof-by-logical-evaluation-1'><b>6.23.</b> Proof by Logical Evaluation</a></li>
<li><a href='05-reflection.html#proof-by-logical-evaluation-2'><b>6.24.</b> Proof by Logical Evaluation</a></li>
<li><a href='05-reflection.html#proof-by-induction'><b>6.25.</b> Proof by Induction</a></li>
<li><a href='05-reflection.html#proof-by-induction-1'><b>6.26.</b> Proof by Induction</a></li>
<li><a href='05-reflection.html#proof-by-induction-2'><b>6.27.</b> Proof by Induction</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-5'><b>6.28.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-6'><b>6.29.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-7'><b>6.30.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#theorems-about-data'><b>6.31.</b> Theorems about Data</a></li>
<li><a href='05-reflection.html#theorems-about-data-associativity-of-append'><b>6.32.</b> Theorems about Data: Associativity of <code>append</code></a></li>
<li><a href='05-reflection.html#case-study-mapreduce'><b>6.33.</b> Case Study: MapReduce</a></li>
<li><a href='05-reflection.html#case-study-mapreduce-1'><b>6.34.</b> Case Study: MapReduce</a></li>
<li><a href='05-reflection.html#reduce-theorem'><b>6.35.</b> Reduce Theorem</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-8'><b>6.36.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#outline'><b>6.37.</b> Outline</a></li>
<li><a href='05-reflection.html#outline-1'><b>6.38.</b> Outline</a></li>
</ul>
<li><a href='06-concl.html'><b>7.</b>LiquidHaskell</a></li>
<ul class='section'>
<li><a href='06-concl.html#liquidhaskell-1'><b>7.1.</b> LiquidHaskell</a></li>
<li><a href='06-concl.html#liquidhaskell-2'><b>7.2.</b> LiquidHaskell</a></li>
<li><a href='06-concl.html#evaluation'><b>7.3.</b> Evaluation</a></li>
<li><a href='06-concl.html#recap-refinement-types'><b>7.4.</b> Recap: Refinement Types</a></li>
<li><a href='06-concl.html#recap-refinement-types-1'><b>7.5.</b> Recap: Refinement Types</a></li>
<li><a href='06-concl.html#recap-refinement-types-2'><b>7.6.</b> Recap: Refinement Types</a></li>
<li><a href='06-concl.html#recap-refinement-types-3'><b>7.7.</b> Recap: Refinement Types</a></li>
<li><a href='06-concl.html#many-friends-many-directions'><b>7.8.</b> Many Friends, Many Directions</a></li>
<li><a href='06-concl.html#thank-you'><b>7.9.</b> Thank You!</a></li>
</ul>
</ul>

</div>

       <div id="checker-status">

         <!-- Verifying ... -->
         <button class="btn btn-xs btn-link actbutton" type="button" style="font-size:30px; z-index:1"
                ng-show="isChecking" ng-click="verifySource()">
          <span class="glyphicon glyphicon-hourglass"></span>
         </button>


         <!-- Safe -->
         <button class="btn btn-xs btn-link actbutton" type="button" style="font-size:30px; color:green; z-index:1"
                 ng-show="isSafe">
           <span class="glyphicon glyphicon-ok"></span>
         </button>

         <div class="dropdown" ng-show="isBad">
             <button class="btn btn-xs btn-link dropdown-toggle"
                     type="button"
                     id="errorblockdropdown"
                     data-toggle="dropdown"
                     style="font-size:30px; color:red; z-index:1">
               <span class="glyphicon glyphicon-remove" style="vertical-align:middle"></span><font size="4">{{errorBlocks.length}}</font>
               </span>
             </button>
             <ul class="dropdown-menu" role="menu" aria-labelledby="dLabel">
               <li ng-repeat="err in errorBlocks">
                 <a tabindex="-1" ng-click="jumpToProgPane(err)">{{err.index}}</a>
               </li>
             </ul>
         </div>
       </div>


<div id='page-wrapper'>
<div id='page'>

<div class="hidden">
<div id="program-pane-0" class="welleditor" style="background:#fff; position:relative">

  <!-- Verify Source -->
  <button class="btn btn-xs btn-link actbutton" type="button" style="z-index:1"
          ng-show="isUnknown" ng-click="verifySource()">
    <span class="glyphicon glyphicon-play"></span>
  </button>
 
  <div id="program-0" class="programbox">{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--short-names"    @-}

module AbstractingRefinements ( insertSort ) where

import Prelude hiding (foldr)

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f b []     = b
foldr f b (x:xs) = f x (foldr f b xs)</div>
</div>

</div>
<div id="slide-0" class="slide">
<h2 id="invariants-in-constructors">Invariants In Constructors</h2>
<div class="mybreak">
<br>
</div>
<p>Many <em>many</em> possibilities ...</p>
</div>
<div id="slide-1" class="slide">
<h2 id="invariants-in-constructors-1">Invariants In Constructors</h2>
<div class="mybreak">
<br>
</div>
<p>Lets specify <strong>ordered lists</strong>:</p>
<div class="hidden">
<div id="program-pane-1" class="welleditor" style="background:#fff; position:relative">

  <!-- Verify Source -->
  <button class="btn btn-xs btn-link actbutton" type="button" style="z-index:1"
          ng-show="isUnknown" ng-click="verifySource()">
    <span class="glyphicon glyphicon-play"></span>
  </button>
 
  <div id="program-1" class="programbox">data OList a = Emp
             | (:<) { hd :: a
                    , tl :: OList a }
infixr 9 :<</div>
</div>

</div>
<div id="program-pane-2" class="welleditor" style="background:#fff; position:relative">

  <!-- Verify Source -->
  <button class="btn btn-xs btn-link actbutton" type="button" style="z-index:1"
          ng-show="isUnknown" ng-click="verifySource()">
    <span class="glyphicon glyphicon-play"></span>
  </button>
 
  <div id="program-2" class="programbox">{-@ data OList a = Emp
                 | (:<) { hd :: a
                        , tl :: OList {v:a | hd <= v}}
  @-}</div>
</div>

</div>
<div id="slide-2" class="slide">
<h2 id="invariants-in-constructors-2">Invariants In Constructors</h2>
<div class="mybreak">
<br>
</div>
<p><strong>Make illegal values unrepresentable!</strong></p>
<div id="program-pane-3" class="welleditor" style="background:#fff; position:relative">

  <!-- Verify Source -->
  <button class="btn btn-xs btn-link actbutton" type="button" style="z-index:1"
          ng-show="isUnknown" ng-click="verifySource()">
    <span class="glyphicon glyphicon-play"></span>
  </button>
 
  <div id="program-3" class="programbox">ok :: OList Int
ok = 1 :< 2 :< 3 :< Emp

bad :: OList Int
bad = 1 :< 3 :< 2 :< Emp</div>
</div>

</div>
<div id="slide-3" class="slide">
<h2 id="invariants-in-constructors-3">Invariants In Constructors</h2>
<div class="mybreak">
<br>
</div>
<p>Make illegal values unrepresentable!</p>
<div class="mybreak">
<br>
</div>
<p>But its tedious to have <strong>multiple list types</strong> ...</p>
</div>
<div id="slide-4" class="slide">
<h2 id="abstracting-refinements">Abstracting Refinements</h2>
<div class="mybreak">
<br>
</div>
<p><strong>Parameterize types over refinements!</strong></p>
</div>
<div id="slide-5" class="slide">
<h2 id="abstracting-refinements-1">Abstracting Refinements</h2>
<div class="mybreak">
<br>
</div>
<p><strong>Parameterize types over refinements!</strong></p>
<div class="mybreak">
<br>
</div>
<pre class="spec"><code>data [a]&lt;p :: a -&gt; a -&gt; Prop&gt; where
  = []
  | (:) { hd :: a
        , tl :: [{v:a | p hd v}]}
</code></pre>
</div>
<div id="slide-6" class="slide">
<h2 id="abstracting-refinements-2">Abstracting Refinements</h2>
<div class="mybreak">
<br>
</div>
<p><strong>Instantiate</strong> refinements to get different invariants!</p>
<div class="mybreak">
<br>
</div>
<div id="program-pane-4" class="welleditor" style="background:#fff; position:relative">

  <!-- Verify Source -->
  <button class="btn btn-xs btn-link actbutton" type="button" style="z-index:1"
          ng-show="isUnknown" ng-click="verifySource()">
    <span class="glyphicon glyphicon-play"></span>
  </button>
 
  <div id="program-4" class="programbox">{-@ type Incrs a = [a]<{\x y -> x <= y}> @-}
{-@ type Decrs a = [a]<{\x y -> x >= y}> @-}
{-@ type Diffs a = [a]<{\x y -> x /= y}> @-}</div>
</div>

</div>
<div id="slide-7" class="slide">
<h2 id="using-abstract-refinements">Using Abstract Refinements</h2>
<div class="mybreak">
<br>
</div>
<p><strong>Inference FTW!</strong></p>
<div class="mybreak">
<br>
</div>
<div id="program-pane-5" class="welleditor" style="background:#fff; position:relative">

  <!-- Verify Source -->
  <button class="btn btn-xs btn-link actbutton" type="button" style="z-index:1"
          ng-show="isUnknown" ng-click="verifySource()">
    <span class="glyphicon glyphicon-play"></span>
  </button>
 
  <div id="program-5" class="programbox">{-@ insertSort :: (Ord a) => [a] -> Incrs a @-}
insertSort xs = foldr insert [] xs

insert x []     = [x]
insert x (y:ys)
  | x < y       = x : y : ys
  | otherwise   = y : insert x ys</div>
</div>

</div>
<div id="slide-8" class="slide">
<h2 id="recap">Recap</h2>
<div class="mybreak">
<br>
</div>
<p><strong>Abstract Refinements</strong></p>
<p>Parametric Polymorphism for Refinement Types</p>
</div>
<div id="slide-9" class="slide">
<h2 id="recap-1">Recap</h2>
<div class="mybreak">
<br>
</div>
<p><strong>Abstract Refinements</strong></p>
<p>Parametric Polymorphism for Refinement Types</p>
<div class="mybreak">
<br>
</div>
<p><strong>Bounded Refinements</strong></p>
<p>Bounded Quantification for Refinement Types</p>
</div>
<div id="slide-10" class="slide">
<h2 id="bounded-refinements-induction-as-a-type">Bounded Refinements: Induction as a Type</h2>
<div class="mybreak">
<br>
</div>
<p>The <strong>bound</strong> <code>Inductive</code> says relation <code>step</code> preserves <code>inv</code></p>
<pre class="spec"><code>Inductive inv step = \y ys acc v -&gt;
  inv ys acc ==&gt; step y acc v ==&gt; inv (y:ys) v
</code></pre>
</div>
<div id="slide-11" class="slide">
<h2 id="bounded-refinements-induction-as-a-type-1">Bounded Refinements: Induction as a Type</h2>
<div class="mybreak">
<br>
</div>
<p>The <strong>bound</strong> <code>Inductive</code> says relation <code>step</code> preserves <code>inv</code></p>
<pre class="spec"><code>Inductive inv step = \y ys acc v -&gt;
  inv ys acc ==&gt; step y acc v ==&gt; inv (y:ys) v
</code></pre>
<p><strong>Key Idea</strong></p>
<p>Bound is a Horn Clause over (Abstract) Refinements</p>
</div>
<div id="slide-12" class="slide">
<h2 id="bounded-refinements-induction-as-a-type-2">Bounded Refinements: Induction as a Type</h2>
<div class="mybreak">
<br>
</div>
<p>The type of <code>foldr</code> encodes <strong>induction over lists</strong> ...</p>
<pre class="spec"><code>foldr :: (Inductive inv step)
      =&gt; (x:a -&gt; acc:b -&gt; b&lt;step x acc&gt;)
      -&gt; b&lt;inv []&gt;
      -&gt; xs:[a]
      -&gt; b&lt;inv xs&gt;
</code></pre>
</div>
<div id="slide-13" class="slide">
<h2 id="bounded-refinements-induction-as-a-type-3">Bounded Refinements: Induction as a Type</h2>
<div class="mybreak">
<br>
</div>
<p>... and lets us verify:</p>
<pre class="spec"><code>insertSort :: (Ord a)
           =&gt; xs:[a]
           -&gt; {v:Incrs a | elts v == elts xs}

insertSort = foldr insert []
</code></pre>
</div>

</div>
</div>

<!--Site Meter
<div class="hidden">
  <script type="text/javascript" src="http://s23.sitemeter.com/js/counter.js?site=s23liquidtypes"></script>
  <noscript>
    <a href="http://s23.sitemeter.com/stats.asp?site=s23liquidtypes"
      target="_top">
      <img src="http://s23.sitemeter.com/meter.asp?site=s23liquidtypes"
      alt="Site Meter" border="0"/></a>
  </noscript>
</div>
-->


<!-- JavaScript below! ============================================== -->

  <script src="./js/ace/ace.js" type="text/javascript" charset="utf-8"></script>
  <script src="./js/ace/theme-monokai.js" type="text/javascript" charset="utf-8"></script>
  <script src="./js/ace/mode-haskell.js"  type="text/javascript" charset="utf-8"></script>
  <script src="./js/liquid/tooltip.js"></script>
  <script src="./js/liquid/annot.js"></script>
  <script src="./js/liquid/config.js"></script>
  <script src="./js/liquid/slideshow.js"></script>
  <script src="./js/liquid/liquid.js"></script>

  <script type="text/javascript">
    var queryServerURL = "http://goto.ucsd.edu:8090/" ;
  </script>

  <!-- rust nav JS -->
  <script type="text/javascript">
    window.playgroundUrl = "";
  </script>

<script type="text/javascript">
document.addEventListener("DOMContentLoaded", function(event) {

 document.getElementById("toggle-nav").onclick = toggleNav;

  function toggleNav() {
    var toc         = document.getElementById("toc");
    var pagewrapper = document.getElementById("page-wrapper");
    var status      = document.getElementById("checker-status");

    toggleClass(toc,         "mobile-hidden");
    // toggleClass(status,      "mobile-hidden");
    toggleClass(pagewrapper, "mobile-hidden");
  };

  function toggleClass(el, className) {
     // from http://youmightnotneedjquery.com/
     if (el.classList) {
       el.classList.toggle(className);
     } else {
       var classes = el.className.split(' ');
       var existingIndex = classes.indexOf(className);

       if (existingIndex >= 0) {
         classes.splice(existingIndex, 1);
       } else {
         classes.push(className);
       }
       el.className = classes.join(' ');
     }
  }
});
</script>


</body>
</html>