why3-doc-html 0.88.3-1ubuntu4 / usr / share / doc / why3-doc-html / html / index.html

This file is indexed.

/usr/share/doc/why3-doc-html/html/index.html is in why3-doc-html 0.88.3-1ubuntu4.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below. 

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
<!DOCTYPE html>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=US-ASCII">
<meta name="generator" content="hevea 2.30">
<title>The Why3 platform
</title>
<link rel="stylesheet" type="text/css" href="manual.css">
</head>
<body>
<!--HEVEA command line is: /usr/bin/hevea -o html/manual.html -fix -O fix.hva makeidx.hva manual.tex -->
<!--HACHA command line is: /usr/bin/hacha -tocbis -o html/index.html html/manual.html -->
<div class="center"><p>
<span style="font-size:xx-large"><span style="font-size:150%"><span style="font-family:sans-serif;font-weight:bold">The Why3 platform</span></span></span></p><p>Version 0.88.3, January 2018
</p><table class="c001 cellpading0"><tr><td class="c013"> Fran&#XE7;ois Bobot<sup>1,2</sup> </td></tr>
<tr><td class="c013"> Jean-Christophe Filli&#XE2;tre<sup>1,2</sup> </td></tr>
<tr><td class="c013"> Claude March&#XE9;<sup>2,1</sup> </td></tr>
<tr><td class="c013"> Guillaume Melquiond<sup>2,1</sup></td></tr>
<tr><td class="c013"> Andrei Paskevich<sup>1,2</sup>
</td></tr>
</table><div class="flushleft"><table class="c001 cellpading0"><tr><td class="c015"><sup>1</sup> LRI, CNRS &amp; University Paris-Sud, Orsay, F-91405 </td></tr>
<tr><td class="c015"><sup>2</sup> Inria Saclay &#X2013; &#XCE;le-de-France, Palaiseau, F-91120
</td></tr>
</table><p>&#XA9;2010&#X2013;2016 University Paris-Sud, CNRS, Inria</p><p>This work has been partly supported by the &#X2018;<a href="http://frama-c.com/u3cat/">U3CAT</a>&#X2019;
national ANR project (ANR-08-SEGI-021-08) ; the &#X2018;<a href="http://www.open-do.org/projects/hi-lite/">Hi-Lite</a>&#X2019;
 FUI project of the
System@tic competitivity cluster ; the &#X2018;<a href="http://bware.lri.fr/">BWare</a>&#X2019;
ANR project (ANR-12-INSE-0010) ; and the <a href="http://www.spark-2014.org/proofinuse">Joint Laboratory ProofInUse</a> (ANR-13-LAB3-0007)
</p></div></div><ul>
<li><a href="foreword.html">Foreword</a>
</li></ul>
<table class="center"><tr><td><h1 class="part" id="sec5">Part&#XA0;I<br>
Tutorial</h1></td></tr>
</table>
<ul>
<li><a href="starting.html">Getting Started</a>
<ul>
<li><a href="starting.html#sec7">Hello Proofs</a>
</li><li><a href="starting.html#sec8">Getting Started with the GUI</a>
</li><li><a href="starting.html#sec14">Getting Started with the <span class="c007">Why3</span> Command</a>
</li></ul>
</li><li><a href="syntax.html">The <span class="c007">Why3</span> Language</a>
<ul>
<li><a href="syntax.html#sec16">Example 1: Lists</a>
</li><li><a href="syntax.html#sec17">Example 1 (continued): Lists and Abstract Orderings</a>
</li><li><a href="syntax.html#sec18">Example 2: Einstein&#X2019;s Problem</a>
</li></ul>
</li><li><a href="whyml.html">The <span class="c007">WhyML</span> Programming Language</a>
<ul>
<li><a href="whyml.html#sec20">Problem 1: Sum and Maximum</a>
</li><li><a href="whyml.html#sec21">Problem 2: Inverting an Injection</a>
</li><li><a href="whyml.html#sec22">Problem 3: Searching a Linked List</a>
</li><li><a href="whyml.html#sec23">Problem 4: N-Queens</a>
</li><li><a href="whyml.html#sec24">Problem 5: Amortized Queue</a>
</li></ul>
</li><li><a href="api.html">The <span class="c007">Why3</span> API</a>
<ul>
<li><a href="api.html#sec26">Building Propositional Formulas</a>
</li><li><a href="api.html#sec27">Building Tasks</a>
</li><li><a href="api.html#sec28">Calling External Provers</a>
</li><li><a href="api.html#sec29">Building Terms</a>
</li><li><a href="api.html#sec30">Building Quantified Formulas</a>
</li><li><a href="api.html#sec31">Building Theories</a>
</li><li><a href="api.html#sec32">Applying Transformations</a>
</li><li><a href="api.html#sec33">Writing New Functions on Terms</a>
</li><li><a href="api.html#sec34">Proof Sessions</a>
</li><li><a href="api.html#sec35">ML Programs</a>
</li></ul>
</li></ul>
<table class="center"><tr><td><h1 class="part" id="sec36">Part&#XA0;II<br>
Reference Manual</h1></td></tr>
</table>
<ul>
<li><a href="install.html">Compilation, Installation</a>
<ul>
<li><a href="install.html#sec38">Installation Instructions from Source Distribution</a>
</li><li><a href="install.html#sec39">Local Use, Without Installation</a>
</li><li><a href="install.html#sec40">Installation of the <span class="c007">Why3</span> API</a>
</li><li><a href="install.html#sec41">Installation of External Provers</a>
</li><li><a href="install.html#sec42">Multiple Versions of the Same Prover</a>
</li><li><a href="install.html#sec43">Session Update after Prover Upgrade</a>
</li></ul>
</li><li><a href="manpages.html">Reference Manuals for the <span class="c007">Why3</span> Tools</a>
<ul>
<li><a href="manpages.html#sec45">The <span class="c003">config</span> Command</a>
</li><li><a href="manpages.html#sec46">The <span class="c003">prove</span> Command</a>
</li><li><a href="manpages.html#sec49">The <span class="c003">ide</span> Command</a>
</li><li><a href="manpages.html#sec56">The <span class="c003">bench</span> Command</a>
</li><li><a href="manpages.html#sec57">The <span class="c003">replay</span> Command</a>
</li><li><a href="manpages.html#sec61">The <span class="c003">session</span> Command</a>
</li><li><a href="manpages.html#sec69">The <span class="c003">doc</span> Command</a>
</li><li><a href="manpages.html#sec72">The <span class="c003">execute</span> Command</a>
</li><li><a href="manpages.html#sec73">The <span class="c003">extract</span> Command</a>
</li><li><a href="manpages.html#sec74">The <span class="c003">realize</span> Command</a>
</li><li><a href="manpages.html#sec75">The <span class="c003">wc</span> Command</a>
</li></ul>
</li><li><a href="syntaxref.html">Language Reference</a>
<ul>
<li><a href="syntaxref.html#sec77">Lexical Conventions</a>
</li><li><a href="syntaxref.html#sec84">The <span class="c007">Why3</span> Language</a>
</li><li><a href="syntaxref.html#sec94">The <span class="c007">WhyML</span> Language</a>
</li><li><a href="syntaxref.html#sec99">The <span class="c007">Why3</span> Standard Library</a>
</li></ul>
</li><li><a href="exec.html">Executing <span class="c007">WhyML</span> Programs</a>
<ul>
<li><a href="exec.html#sec101">Interpreting <span class="c007">WhyML</span> Code</a>
</li><li><a href="exec.html#sec102">Compiling <span class="c007">WhyML</span> to OCaml</a>
</li></ul>
</li><li><a href="itp.html">Interactive Proof Assistants</a>
<ul>
<li><a href="itp.html#sec104">Using an Interactive Proof Assistant to Discharge Goals</a>
</li><li><a href="itp.html#sec105">Theory Realizations</a>
</li><li><a href="itp.html#sec109">Coq</a>
</li><li><a href="itp.html#sec114">Isabelle/HOL</a>
</li><li><a href="itp.html#sec118">PVS</a>
</li></ul>
</li><li><a href="technical.html">Technical Informations</a>
<ul>
<li><a href="technical.html#sec123">Structure of Session Files</a>
</li><li><a href="technical.html#sec124">Prover Detection</a>
</li><li><a href="technical.html#sec125">The <span class="c003">why3.conf</span> Configuration File</a>
</li><li><a href="technical.html#sec126">Drivers for External Provers</a>
</li><li><a href="technical.html#sec127">Transformations</a>
</li><li><a href="technical.html#sec136">Proof Strategies</a>
</li></ul>
</li></ul>
<table class="center"><tr><td><h1 class="part" id="sec137">Part&#XA0;III<br>
Appendix</h1></td></tr>
</table>
<ul>
<li><a href="changes.html">Release Notes</a>
<ul>
<li><a href="changes.html#sec139">Release Notes for version 0.80: syntax changes w.r.t. 0.73</a>
</li><li><a href="changes.html#sec140">Summary of Changes w.r.t. Why 2</a>
</li></ul>
</li><li><a href="manual013.html">References</a>
</li><li><a href="manual014.html">Index</a>
</li></ul>
<!--FOOTER-->
<hr style="height:2"><blockquote class="quote"><em>This document was translated from L<sup>A</sup>T<sub>E</sub>X by
</em><a href="http://hevea.inria.fr/index.html"><em>H<span class="c008"><sup>E</sup></span>V<span class="c008"><sup>E</sup></span>A</em></a><em>.</em></blockquote></body>
</html>

APT Browse - Built by Thomas Orozco.