<div class="xblock xblock-public_view xblock-public_view-vertical" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@vertical+block@vertical-designing-specifications-objectives" data-block-type="vertical" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">Reading 5 Objectives</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+6.005.1x+3T2016+type@video+block@video_f66c81b86236">
<div class="xblock xblock-public_view xblock-public_view-video xmodule_display xmodule_VideoBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@video+block@video_f66c81b86236" data-block-type="video" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Video"}
</script>
<h3 class="hd hd-2">Video</h3>
<div
id="video_video_f66c81b86236"
class="video closed"
data-metadata='{"transcriptLanguages": {"en": "English"}, "lmsRootURL": "https://openlearninglibrary.mit.edu", "captionDataDir": null, "ytTestTimeout": 1500, "saveStateEnabled": false, "start": 0.0, "autoAdvance": false, "ytApiUrl": "https://www.youtube.com/iframe_api", "ytMetadataEndpoint": "", "recordedYoutubeIsAvailable": true, "speed": null, "generalSpeed": 1.0, "streams": "1.00:yUXNMmmimoY", "completionEnabled": false, "end": 0.0, "transcriptTranslationUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_f66c81b86236/handler/transcript/translation/__lang__", "prioritizeHls": false, "duration": 37.08, "publishCompletionUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_f66c81b86236/handler/publish_completion", "completionPercentage": 0.95, "transcriptAvailableTranslationsUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_f66c81b86236/handler/transcript/available_translations", "showCaptions": "true", "saveStateUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_f66c81b86236/handler/xmodule_handler/save_user_state", "poster": null, "autoplay": false, "transcriptLanguage": "en", "autohideHtml5": false, "savedVideoPosition": 0.0, "sources": ["https://d2f1egay8yehza.cloudfront.net/MIT600512016-V002800_DTH.mp4", "https://d2f1egay8yehza.cloudfront.net/MIT600512016-V002800/MIT600512016-V002800.m3u8"]}'
data-bumper-metadata='null'
data-autoadvance-enabled="False"
data-poster='null'
tabindex="-1"
>
<div class="focus_grabber first"></div>
<div class="tc-wrapper">
<div class="video-wrapper">
<span tabindex="0" class="spinner" aria-hidden="false" aria-label="Loading video player"></span>
<span tabindex="-1" class="btn-play fa fa-youtube-play fa-2x is-hidden" aria-hidden="true" aria-label="Play video"></span>
<div class="video-player-pre"></div>
<div class="video-player">
<div id="video_f66c81b86236"></div>
<h4 class="hd hd-4 video-error is-hidden">No playable video sources found.</h4>
<h4 class="hd hd-4 video-hls-error is-hidden">
Your browser does not support this video format. Try using a different browser.
</h4>
</div>
<div class="video-player-post"></div>
<div class="closed-captions"></div>
<div class="video-controls is-hidden">
<div>
<div class="vcr"><div class="vidtime">0:00 / 0:00</div></div>
<div class="secondary-controls"></div>
</div>
</div>
</div>
</div>
<div class="focus_grabber last"></div>
<h3 class="hd hd-4 downloads-heading sr" id="video-download-transcripts_video_f66c81b86236">Downloads and transcripts</h3>
<div class="wrapper-downloads" role="region" aria-labelledby="video-download-transcripts_video_f66c81b86236">
<div class="wrapper-download-transcripts">
<h4 class="hd hd-5">Transcripts</h4>
<ul class="list-download-transcripts">
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_f66c81b86236/handler/transcript/download" data-value="srt">Download SubRip (.srt) file</a>
</li>
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_f66c81b86236/handler/transcript/download" data-value="txt">Download Text (.txt) file</a>
</li>
</ul>
</div>
</div>
</div>
</div>
</div>
<div class="vert vert-1" data-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_6f7f450863c1">
<div class="xblock xblock-public_view xblock-public_view-html xmodule_display xmodule_HtmlBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_6f7f450863c1" data-block-type="html" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "HTMLModule"}
</script>
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<h4>Software in 6.005</h4>
<table class="table table-striped no-markdown">
<tbody>
<tr>
<th width="33%">Safe from bugs</th>
<th>Easy to understand</th>
<th>Ready for change</th>
</tr>
<tr>
<td>
Correct today and correct in the unknown future
</td>
<td>
Communicates clearly with future programmers, including future you
</td>
<td>
Designed to accommodate change without rewriting
</td>
</tr>
</tbody>
</table>
<h4>Objectives for Today</h4>
<p>Today we continue our discussion of specifications, by talking more about the properties of specs, and what makes some specs better than others.</p>
<p>After today’s reading, you should:</p>
<ul>
<li>Understand underdetermined specs and be able to identify and assess nondeterminism</li>
<li>Understand declarative vs. operational specs and be able to write declarative specs</li>
<li>Understand strength of preconditions, postconditions, and specs; and be able to compare spec strength</li>
<li>Be able to write coherent, useful specifications of appropriate strength</li>
</ul>
</div>
</div>
</div>
</div>
<div class="xblock xblock-public_view xblock-public_view-vertical" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@vertical+block@Deterministic_vs._Underdetermined_Specs" data-block-type="vertical" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">Deterministic vs. Underdetermined Specs</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+6.005.1x+3T2016+type@video+block@video_bc042e7e29ef">
<div class="xblock xblock-public_view xblock-public_view-video xmodule_display xmodule_VideoBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@video+block@video_bc042e7e29ef" data-block-type="video" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Video"}
</script>
<h3 class="hd hd-2">Video</h3>
<div
id="video_video_bc042e7e29ef"
class="video closed"
data-metadata='{"transcriptLanguages": {"en": "English"}, "lmsRootURL": "https://openlearninglibrary.mit.edu", "captionDataDir": null, "ytTestTimeout": 1500, "saveStateEnabled": false, "start": 0.0, "autoAdvance": false, "ytApiUrl": "https://www.youtube.com/iframe_api", "ytMetadataEndpoint": "", "recordedYoutubeIsAvailable": true, "speed": null, "generalSpeed": 1.0, "streams": "1.00:Tpyzb64wdhA", "completionEnabled": false, "end": 0.0, "transcriptTranslationUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_bc042e7e29ef/handler/transcript/translation/__lang__", "prioritizeHls": false, "duration": 318.93, "publishCompletionUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_bc042e7e29ef/handler/publish_completion", "completionPercentage": 0.95, "transcriptAvailableTranslationsUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_bc042e7e29ef/handler/transcript/available_translations", "showCaptions": "true", "saveStateUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_bc042e7e29ef/handler/xmodule_handler/save_user_state", "poster": null, "autoplay": false, "transcriptLanguage": "en", "autohideHtml5": false, "savedVideoPosition": 0.0, "sources": ["https://d2f1egay8yehza.cloudfront.net/MIT600512016-V003200_DTH.mp4", "https://d2f1egay8yehza.cloudfront.net/MIT600512016-V003200/MIT600512016-V003200.m3u8"]}'
data-bumper-metadata='null'
data-autoadvance-enabled="False"
data-poster='null'
tabindex="-1"
>
<div class="focus_grabber first"></div>
<div class="tc-wrapper">
<div class="video-wrapper">
<span tabindex="0" class="spinner" aria-hidden="false" aria-label="Loading video player"></span>
<span tabindex="-1" class="btn-play fa fa-youtube-play fa-2x is-hidden" aria-hidden="true" aria-label="Play video"></span>
<div class="video-player-pre"></div>
<div class="video-player">
<div id="video_bc042e7e29ef"></div>
<h4 class="hd hd-4 video-error is-hidden">No playable video sources found.</h4>
<h4 class="hd hd-4 video-hls-error is-hidden">
Your browser does not support this video format. Try using a different browser.
</h4>
</div>
<div class="video-player-post"></div>
<div class="closed-captions"></div>
<div class="video-controls is-hidden">
<div>
<div class="vcr"><div class="vidtime">0:00 / 0:00</div></div>
<div class="secondary-controls"></div>
</div>
</div>
</div>
</div>
<div class="focus_grabber last"></div>
<h3 class="hd hd-4 downloads-heading sr" id="video-download-transcripts_video_bc042e7e29ef">Downloads and transcripts</h3>
<div class="wrapper-downloads" role="region" aria-labelledby="video-download-transcripts_video_bc042e7e29ef">
<div class="wrapper-download-transcripts">
<h4 class="hd hd-5">Transcripts</h4>
<ul class="list-download-transcripts">
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_bc042e7e29ef/handler/transcript/download" data-value="srt">Download SubRip (.srt) file</a>
</li>
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_bc042e7e29ef/handler/transcript/download" data-value="txt">Download Text (.txt) file</a>
</li>
</ul>
</div>
</div>
</div>
</div>
</div>
<div class="vert vert-1" data-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_d4af89dfb27c">
<div class="xblock xblock-public_view xblock-public_view-html xmodule_display xmodule_HtmlBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_d4af89dfb27c" data-block-type="html" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "HTMLModule"}
</script>
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<h2 id="introduction">Introduction</h2>
<div data-outline="introduction">
<p>In this reading we'll look at different specs for similar behaviors, and talk about the tradeoffs between them. We'll look at three dimensions for comparing specs:</p>
<ul>
<li>
<p>How <strong>deterministic</strong> it is. Does the spec define only a single possible output for a given input, or does it allow the implementor to choose from a set of legal outputs?</p>
</li>
<li>
<p>How <strong>declarative</strong> it is. Does the spec just characterize <em>what</em> the output should be, or does it explicitly say <em>how</em> to compute the output?</p>
</li>
<li>
<p>How <strong>strong</strong> it is. Does the spec have a small set of legal implementations, or a large set?</p>
</li>
</ul>
<p>Not all specifications we might choose for a module are equally useful, and we'll explore what makes some specifications better than others.</p>
</div>
<h2 id="deterministic_vs_underdetermined_specs">Deterministic vs. underdetermined specs</h2>
<div data-outline="deterministic_vs_underdetermined_specs">
<p>Recall the two example implementations of <code>find</code> we began with in an <a href="/courses/course-v1:MITx+6.005.1x+3T2016/jump_to_id/vertical-why-specifications">earlier reading</a>:</p><pre class="no-markdown"><code>static int find<sub>First</sub>(int[] arr, int val) {
for (int i = 0; i < arr.length; i++) {
if (arr[i] == val) return i;
}
return arr.length;
}
</code></pre><pre class="no-markdown"><code>static int find<sub>Last</sub>(int[] arr, int val) {
for (int i = arr.length - 1 ; i >= 0; i--) {
if (arr[i] == val) return i;
}
return -1;
}
</code></pre>
<p>The subscripts <code class="no-markdown"><sub>First</sub></code> and <code class="no-markdown"><sub>Last</sub></code> are not actual Java syntax. We're using them here to distinguish the two implementations for the sake of discussion. In the actual code, both implementations should be Java methods called <code>find</code>.</p>
<p>Here is one possible specification of <code>find</code>:</p><pre class="no-markdown">static int find<sub>ExactlyOne</sub>(int[] arr, int val)
<em>requires</em>: val occurs <strong>exactly once</strong> in arr
<em>effects</em>: returns index i such that arr[i] = val
</pre>
<p>This specification is <strong>deterministic</strong>: when presented with a state satisfying the precondition, the outcome is completely determined. Only one return value and one final state are possible. There are no valid inputs for which there is more than one valid output.</p>
<p>Both <code class="no-markdown">find<sub>First</sub></code> and <code class="no-markdown">find<sub>Last</sub></code> satisfy the specification, so if this is the specification on which the clients relied, the two implementations are equivalent and substitutable for one another.</p>
<p>Here is a slightly different specification:</p><pre class="no-markdown">static int find<sub>OneOrMore,AnyIndex</sub>(int[] arr, int val)
<em>requires</em>: val occurs in arr
<em>effects</em>: returns index i such that arr[i] = val
</pre>
<p>This specification is not deterministic. It doesn't say which index is returned if <code>val</code> occurs more than once. It simply says that if you look up the entry at the index given by the returned value, you'll find <code>val</code>. This specification allows multiple valid outputs for the same input.</p>
<p>Note that this is different from <em>nondeterministic</em> in the usual sense of that word. Nondeterministic code sometimes behaves one way and sometimes another, even if called in the same program with the same inputs. This can happen, for example, when the code's behavior depends on a random number, or when it depends on the timing of concurrent processes. But a specification which is not deterministic doesn't have to have a nondeterministic implementation. It can be satisfied by a fully deterministic implementation.</p>
<p>To avoid the confusion, we'll refer to specifications that are not deterministic as <strong>underdetermined</strong>.</p>
<p>This underdetermined <code>find</code> spec is again satisfied by both <code class="no-markdown">find<sub>First</sub></code> and <code class="no-markdown">find<sub>Last</sub></code>, each resolving the underdeterminedness in its own (fully deterministic) way. A client of <code class="no-markdown">find<sub>OneOrMore,AnyIndex</sub></code> spec can't rely on which index will be returned if <code>val</code> appears more than once. The spec would be satisfied by a nondeterministic implementation, too — for example, one that tosses a coin to decide whether to start searching from the beginning or the end of the array. But in almost all cases we'll encounter, underdeterminism in specifications offers a choice that is made by the implementor at implementation time. An underdetermined spec is typically implemented by a fully-deterministic implementation.</p>
</div>
</div>
</div>
</div>
</div>
<div class="xblock xblock-public_view xblock-public_view-vertical" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@vertical+block@vertical_Questions_64360239142b" data-block-type="vertical" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">Questions</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_fff67ba8819a">
<div class="xblock xblock-public_view xblock-public_view-html xmodule_display xmodule_HtmlBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_fff67ba8819a" data-block-type="html" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "HTMLModule"}
</script>
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<script src="/assets/courseware/v1/3e6443fb95285d2dc06e8ffc448b9bdf/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism.js"></script>
<script src="/assets/courseware/v1/2ba76f8bdfef4e2d45e31a3dc5208470/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/edx-script-v1.js"></script>
</div>
</div>
<div class="vert vert-1" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-distinguished">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-distinguished" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-distinguished" class="problems-wrapper" role="group"
aria-labelledby="05-distinguished-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-distinguished" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-distinguished/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="2"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-distinguished-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-distinguished-problem-progress" tabindex="-1">
distinguished
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-distinguished-problem-progress"></div>
<div class="problem">
<div>
<p>We just saw the following implementations:</p>
<pre class="code">
static int findFirst(int[] arr, int val) {
for (int i = 0; i &lt; arr.length; i++) {
if (arr[i] == val) return i;
}
return arr.length;
}
</pre>
<pre class="code">
static int findLast(int[] arr, int val) {
for (int i = arr.length -1 ; i &gt;= 0; i--) {
if (arr[i] == val) return i;
}
return -1;
}
</pre>
<p>Now consider this possible specification of <code>find</code>:</p>
<pre class="code">
static int find(int[] arr, int val)
requires: nothing
effects: returns largest index i such that
arr[i] = val, or -1 if no such i
</pre>
<p>Which input(s) demonstrate that <code>findFirst</code> does not satisfy this spec? Check all that apply.</p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-distinguished_2_1">
<fieldset aria-describedby="status_05-distinguished_2_1">
<div class="field">
<input type="checkbox" name="input_05-distinguished_2_1[]" id="input_05-distinguished_2_1_choice_0" class="field-input input-checkbox" value="choice_0"/><label id="05-distinguished_2_1-choice_0-label" for="input_05-distinguished_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-distinguished_2_1">
<code>[ 1, 2, 2 ], 2</code>
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-distinguished_2_1[]" id="input_05-distinguished_2_1_choice_1" class="field-input input-checkbox" value="choice_1"/><label id="05-distinguished_2_1-choice_1-label" for="input_05-distinguished_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-distinguished_2_1">
<code>[ 1, 2, 3 ], 2</code>
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-distinguished_2_1[]" id="input_05-distinguished_2_1_choice_2" class="field-input input-checkbox" value="choice_2"/><label id="05-distinguished_2_1-choice_2-label" for="input_05-distinguished_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-distinguished_2_1">
<code>[ 1, 2, 3 ], 4</code>
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-distinguished_2_1[]" id="input_05-distinguished_2_1_choice_3" class="field-input input-checkbox" value="choice_3"/><label id="05-distinguished_2_1-choice_3-label" for="input_05-distinguished_2_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-distinguished_2_1"> none of the above, <code>findFirst</code> does satisfy this spec!
</label>
</div>
<span id="answer_05-distinguished_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-distinguished_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<p>Which input(s) demonstrate that <code>findLast</code> does not satisfy this spec? Check all that apply.</p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 2" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-distinguished_3_1">
<fieldset aria-describedby="status_05-distinguished_3_1">
<div class="field">
<input type="checkbox" name="input_05-distinguished_3_1[]" id="input_05-distinguished_3_1_choice_0" class="field-input input-checkbox" value="choice_0"/><label id="05-distinguished_3_1-choice_0-label" for="input_05-distinguished_3_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-distinguished_3_1">
<code>[ 1, 2, 2 ], 2</code>
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-distinguished_3_1[]" id="input_05-distinguished_3_1_choice_1" class="field-input input-checkbox" value="choice_1"/><label id="05-distinguished_3_1-choice_1-label" for="input_05-distinguished_3_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-distinguished_3_1">
<code>[ 1, 2, 3 ], 2</code>
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-distinguished_3_1[]" id="input_05-distinguished_3_1_choice_2" class="field-input input-checkbox" value="choice_2"/><label id="05-distinguished_3_1-choice_2-label" for="input_05-distinguished_3_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-distinguished_3_1">
<code>[ 1, 2, 3 ], 4</code>
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-distinguished_3_1[]" id="input_05-distinguished_3_1_choice_3" class="field-input input-checkbox" value="choice_3"/><label id="05-distinguished_3_1-choice_3-label" for="input_05-distinguished_3_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-distinguished_3_1"> none of the above, <code>findLast</code> does satisfy the spec!
</label>
</div>
<span id="answer_05-distinguished_3_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-distinguished_3_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-distinguished_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="distinguished" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-distinguished" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-distinguished">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-distinguished-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-distinguished-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-distinguished-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-2" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-a">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-a" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-over-under-a" class="problems-wrapper" role="group"
aria-labelledby="05-over-under-a-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-a" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-a/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-over-under-a-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-a-problem-progress" tabindex="-1">
over/under (a)
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-a-problem-progress"></div>
<div class="problem">
<div>
<p>Previously we saw this <em>under-determined</em> version of the <em>find</em> specification: (let's call it <em>findUnderdet</em>)</p>
<pre class="code">
static int findUnderdet(int[] arr, int val)
requires: val occurs in arr
effects: returns index i such that arr[i] = val
</pre>
<p>This spec allows multiple possible return values for arrays with duplicate values.</p>
<p>For each spec below, say whether it is <em>less</em> fully-determined than <em>findUnderdet</em>, <em>more</em> fully-determined, or deterministic.</p>
<pre class="code">
static int find(int[] arr, int val)
requires: val occurs exactly once in arr
effects: returns index i such that arr[i] = val
</pre>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-over-under-a_2_1">
<fieldset aria-describedby="status_05-over-under-a_2_1">
<div class="field">
<input type="radio" name="input_05-over-under-a_2_1" id="input_05-over-under-a_2_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-over-under-a_2_1-choice_0-label" for="input_05-over-under-a_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-over-under-a_2_1"> deterministic
</label>
</div>
<div class="field">
<input type="radio" name="input_05-over-under-a_2_1" id="input_05-over-under-a_2_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-over-under-a_2_1-choice_1-label" for="input_05-over-under-a_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-over-under-a_2_1"> more fully-determined than <em>findUnderdet</em>, but not deterministic
</label>
</div>
<div class="field">
<input type="radio" name="input_05-over-under-a_2_1" id="input_05-over-under-a_2_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-over-under-a_2_1-choice_2-label" for="input_05-over-under-a_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-over-under-a_2_1"> less fully-determined than <em>findUnderdet</em>
</label>
</div>
<span id="answer_05-over-under-a_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-over-under-a_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-over-under-a_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="over/under (a)" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-over-under-a" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-over-under-a">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-over-under-a-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-over-under-a-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-over-under-a-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-3" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-b">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-b" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-over-under-b" class="problems-wrapper" role="group"
aria-labelledby="05-over-under-b-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-b" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-b/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-over-under-b-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-b-problem-progress" tabindex="-1">
over/under (b)
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-b-problem-progress"></div>
<div class="problem">
<div>
<pre class="code">
static int find(int[] arr, int val)
requires: nothing
effects: returns largest index i such that arr[i] = val, or -1 if no such i
</pre>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-over-under-b_2_1">
<fieldset aria-describedby="status_05-over-under-b_2_1">
<div class="field">
<input type="radio" name="input_05-over-under-b_2_1" id="input_05-over-under-b_2_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-over-under-b_2_1-choice_0-label" for="input_05-over-under-b_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-over-under-b_2_1"> deterministic
</label>
</div>
<div class="field">
<input type="radio" name="input_05-over-under-b_2_1" id="input_05-over-under-b_2_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-over-under-b_2_1-choice_1-label" for="input_05-over-under-b_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-over-under-b_2_1"> more fully-determined than <em>findUnderdet</em>, but not deterministic
</label>
</div>
<div class="field">
<input type="radio" name="input_05-over-under-b_2_1" id="input_05-over-under-b_2_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-over-under-b_2_1-choice_2-label" for="input_05-over-under-b_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-over-under-b_2_1"> less fully-determined than <em>findUnderdet</em>
</label>
</div>
<span id="answer_05-over-under-b_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-over-under-b_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-over-under-b_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="over/under (b)" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-over-under-b" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-over-under-b">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-over-under-b-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-over-under-b-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-over-under-b-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-4" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-c">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-c" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-over-under-c" class="problems-wrapper" role="group"
aria-labelledby="05-over-under-c-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-c" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-c/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-over-under-c-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-c-problem-progress" tabindex="-1">
over/under (c)
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-over-under-c-problem-progress"></div>
<div class="problem">
<div>
<pre class="code">
static int find(int[] arr, int val)
requires: val occurs in arr
effects: returns largest index i such that arr[i] = val
</pre>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-over-under-c_2_1">
<fieldset aria-describedby="status_05-over-under-c_2_1">
<div class="field">
<input type="radio" name="input_05-over-under-c_2_1" id="input_05-over-under-c_2_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-over-under-c_2_1-choice_0-label" for="input_05-over-under-c_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-over-under-c_2_1"> deterministic
</label>
</div>
<div class="field">
<input type="radio" name="input_05-over-under-c_2_1" id="input_05-over-under-c_2_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-over-under-c_2_1-choice_1-label" for="input_05-over-under-c_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-over-under-c_2_1"> more fully-determined than <em>findUnderdet</em>, but not deterministic
</label>
</div>
<div class="field">
<input type="radio" name="input_05-over-under-c_2_1" id="input_05-over-under-c_2_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-over-under-c_2_1-choice_2-label" for="input_05-over-under-c_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-over-under-c_2_1"> less fully-determined than <em>findUnderdet</em>
</label>
</div>
<span id="answer_05-over-under-c_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-over-under-c_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-over-under-c_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="over/under (c)" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-over-under-c" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-over-under-c">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-over-under-c-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-over-under-c-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-over-under-c-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
</div>
</div>
<div class="xblock xblock-public_view xblock-public_view-vertical" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@vertical+block@Declarative_vs._Operational_Specs" data-block-type="vertical" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">Declarative vs. Operational Specs</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+6.005.1x+3T2016+type@video+block@video_d35f22fd6b66">
<div class="xblock xblock-public_view xblock-public_view-video xmodule_display xmodule_VideoBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@video+block@video_d35f22fd6b66" data-block-type="video" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Video"}
</script>
<h3 class="hd hd-2">Video</h3>
<div
id="video_video_d35f22fd6b66"
class="video closed"
data-metadata='{"transcriptLanguages": {"en": "English"}, "lmsRootURL": "https://openlearninglibrary.mit.edu", "captionDataDir": null, "ytTestTimeout": 1500, "saveStateEnabled": false, "start": 0.0, "autoAdvance": false, "ytApiUrl": "https://www.youtube.com/iframe_api", "ytMetadataEndpoint": "", "recordedYoutubeIsAvailable": true, "speed": null, "generalSpeed": 1.0, "streams": "1.00:xgSKzScqSp0", "completionEnabled": false, "end": 0.0, "transcriptTranslationUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_d35f22fd6b66/handler/transcript/translation/__lang__", "prioritizeHls": false, "duration": 169.72, "publishCompletionUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_d35f22fd6b66/handler/publish_completion", "completionPercentage": 0.95, "transcriptAvailableTranslationsUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_d35f22fd6b66/handler/transcript/available_translations", "showCaptions": "true", "saveStateUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_d35f22fd6b66/handler/xmodule_handler/save_user_state", "poster": null, "autoplay": false, "transcriptLanguage": "en", "autohideHtml5": false, "savedVideoPosition": 0.0, "sources": ["https://d2f1egay8yehza.cloudfront.net/MIT600512016-V002500_DTH.mp4", "https://d2f1egay8yehza.cloudfront.net/MIT600512016-V002500/MIT600512016-V002500.m3u8"]}'
data-bumper-metadata='null'
data-autoadvance-enabled="False"
data-poster='null'
tabindex="-1"
>
<div class="focus_grabber first"></div>
<div class="tc-wrapper">
<div class="video-wrapper">
<span tabindex="0" class="spinner" aria-hidden="false" aria-label="Loading video player"></span>
<span tabindex="-1" class="btn-play fa fa-youtube-play fa-2x is-hidden" aria-hidden="true" aria-label="Play video"></span>
<div class="video-player-pre"></div>
<div class="video-player">
<div id="video_d35f22fd6b66"></div>
<h4 class="hd hd-4 video-error is-hidden">No playable video sources found.</h4>
<h4 class="hd hd-4 video-hls-error is-hidden">
Your browser does not support this video format. Try using a different browser.
</h4>
</div>
<div class="video-player-post"></div>
<div class="closed-captions"></div>
<div class="video-controls is-hidden">
<div>
<div class="vcr"><div class="vidtime">0:00 / 0:00</div></div>
<div class="secondary-controls"></div>
</div>
</div>
</div>
</div>
<div class="focus_grabber last"></div>
<h3 class="hd hd-4 downloads-heading sr" id="video-download-transcripts_video_d35f22fd6b66">Downloads and transcripts</h3>
<div class="wrapper-downloads" role="region" aria-labelledby="video-download-transcripts_video_d35f22fd6b66">
<div class="wrapper-download-transcripts">
<h4 class="hd hd-5">Transcripts</h4>
<ul class="list-download-transcripts">
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_d35f22fd6b66/handler/transcript/download" data-value="srt">Download SubRip (.srt) file</a>
</li>
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_d35f22fd6b66/handler/transcript/download" data-value="txt">Download Text (.txt) file</a>
</li>
</ul>
</div>
</div>
</div>
</div>
</div>
<div class="vert vert-1" data-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_54061550e068">
<div class="xblock xblock-public_view xblock-public_view-html xmodule_display xmodule_HtmlBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_54061550e068" data-block-type="html" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "HTMLModule"}
</script>
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<h2 id="declarative_vs_operational_specs">Declarative vs. operational specs</h2>
<div data-outline="declarative_vs_operational_specs">
<p>Roughly speaking, there are two kinds of specifications.
<em>Operational</em> specifications give a series of steps that the method performs; pseudocode descriptions are operational.
<em>Declarative</em> specifications don't give details of intermediate steps. Instead, they just give properties of the final outcome and how it's related to the initial state.</p>
<p>Almost always, declarative specifications are preferable. They're usually shorter, easier to understand, and most importantly, they don't inadvertently expose implementation details that a client may rely on (and then find no longer hold when the implementation is changed). For example, if we want to allow either implementation of <code>find</code>, we would <em>not</em> want to say in the spec that the method “goes down the array until it finds <code>val</code>,” since aside from being rather vague, this spec suggests that the search proceeds from lower to higher indices and that the lowest will be returned, which perhaps the specifier did not intend.</p>
<p>One reason programmers sometimes lapse into operational specifications is because they're using the spec comment to explain the implementation for a maintainer. Don't do that. When it's necessary, use comments within the body of the method, not in the spec comment.</p>
<p>For a given specification, there may be many ways to express it declaratively:</p><pre class="no-markdown">static boolean startsWith(String str, String prefix)
<em>effects</em>: returns true if and only if there exists String suffix
such that prefix + suffix == str
</pre><pre class="no-markdown">static boolean startsWith(String str, String prefix)
<em>effects</em>: returns true if and only if there exists integer i
such that str.substring(0, i) == prefix
</pre><pre class="no-markdown">static boolean startsWith(String str, String prefix)
<em>effects</em>: returns true if the first prefix.length() characters of str
are the characters of prefix, false otherwise
</pre>
<p>It's up to us to choose the clearest specification for clients and maintainers of the code.</p>
</div>
</div>
</div>
</div>
</div>
<div class="xblock xblock-public_view xblock-public_view-vertical" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@vertical+block@vertical_Questions_3cd34d48a890" data-block-type="vertical" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">Questions</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_fff67ba8819a">
<div class="xblock xblock-public_view xblock-public_view-html xmodule_display xmodule_HtmlBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_fff67ba8819a" data-block-type="html" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "HTMLModule"}
</script>
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<script src="/assets/courseware/v1/3e6443fb95285d2dc06e8ffc448b9bdf/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism.js"></script>
<script src="/assets/courseware/v1/2ba76f8bdfef4e2d45e31a3dc5208470/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/edx-script-v1.js"></script>
</div>
</div>
<div class="vert vert-1" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-joint-declaration">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-joint-declaration" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-joint-declaration" class="problems-wrapper" role="group"
aria-labelledby="05-joint-declaration-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-joint-declaration" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-joint-declaration/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-joint-declaration-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-joint-declaration-problem-progress" tabindex="-1">
joint declaration
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-joint-declaration-problem-progress"></div>
<div class="problem">
<div>
<p>Given this specification:</p>
<pre class="code">
static String join(String delimiter, String[] elements)
effects: append together the strings in elements, but at each step,
if there are more elements left, insert delimiter
</pre>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-joint-declaration_2_1">
<fieldset aria-describedby="status_05-joint-declaration_2_1">
<legend id="05-joint-declaration_2_1-legend" class="response-fieldset-legend field-group-hd">Rewrite the spec so it is declarative, not operational.</legend>
<div class="field">
<input type="radio" name="input_05-joint-declaration_2_1" id="input_05-joint-declaration_2_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-joint-declaration_2_1-choice_0-label" for="input_05-joint-declaration_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-joint-declaration_2_1">
<pre>effects: returns the result of adding all elements to a<br/> new StringJoiner(delimiter)</pre>
</label>
</div>
<div class="field">
<input type="radio" name="input_05-joint-declaration_2_1" id="input_05-joint-declaration_2_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-joint-declaration_2_1-choice_1-label" for="input_05-joint-declaration_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-joint-declaration_2_1">
<pre>effects: returns the result of looping through elements and<br/> alternately appending an element and the delimiter</pre>
</label>
</div>
<div class="field">
<input type="radio" name="input_05-joint-declaration_2_1" id="input_05-joint-declaration_2_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-joint-declaration_2_1-choice_2-label" for="input_05-joint-declaration_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-joint-declaration_2_1">
<pre>effects: returns elements joined together with copies of delimiter, i.e.<br/> elements[0] + delimiter + elements[1] + delimiter<br/> + ... + delimiter + elements[elements.length-1]</pre>
</label>
</div>
<span id="answer_05-joint-declaration_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-joint-declaration_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-joint-declaration_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="joint declaration" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-joint-declaration" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-joint-declaration">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-joint-declaration-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-joint-declaration-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-joint-declaration-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-2" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-out-of-joint">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-out-of-joint" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-out-of-joint" class="problems-wrapper" role="group"
aria-labelledby="05-out-of-joint-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-out-of-joint" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-out-of-joint/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-out-of-joint-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-out-of-joint-problem-progress" tabindex="-1">
out of joint
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-out-of-joint-problem-progress"></div>
<div class="problem">
<div>
<p>Which are valid criticisms of the declarative spec from the previous problem? Check all that apply.</p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-out-of-joint_2_1">
<fieldset aria-describedby="status_05-out-of-joint_2_1">
<div class="field">
<input type="checkbox" name="input_05-out-of-joint_2_1[]" id="input_05-out-of-joint_2_1_choice_0" class="field-input input-checkbox" value="choice_0"/><label id="05-out-of-joint_2_1-choice_0-label" for="input_05-out-of-joint_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-out-of-joint_2_1"> Be more clear about the empty delimiter special case
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-out-of-joint_2_1[]" id="input_05-out-of-joint_2_1_choice_1" class="field-input input-checkbox" value="choice_1"/><label id="05-out-of-joint_2_1-choice_1-label" for="input_05-out-of-joint_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-out-of-joint_2_1"> Be more clear about the empty elements special case
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-out-of-joint_2_1[]" id="input_05-out-of-joint_2_1_choice_2" class="field-input input-checkbox" value="choice_2"/><label id="05-out-of-joint_2_1-choice_2-label" for="input_05-out-of-joint_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-out-of-joint_2_1"> Be less deterministic, implementors need more freedom
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-out-of-joint_2_1[]" id="input_05-out-of-joint_2_1_choice_3" class="field-input input-checkbox" value="choice_3"/><label id="05-out-of-joint_2_1-choice_3-label" for="input_05-out-of-joint_2_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-out-of-joint_2_1"> Be more deterministic, clients need more specific results
</label>
</div>
<span id="answer_05-out-of-joint_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-out-of-joint_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-out-of-joint_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="out of joint" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-out-of-joint" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-out-of-joint">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-out-of-joint-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-out-of-joint-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-out-of-joint-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
</div>
</div>
<div class="xblock xblock-public_view xblock-public_view-vertical" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@vertical+block@Stronger_vs._Weaker_Specs" data-block-type="vertical" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">Stronger vs. Weaker Specs</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+6.005.1x+3T2016+type@video+block@video_5feb0a6c6f49">
<div class="xblock xblock-public_view xblock-public_view-video xmodule_display xmodule_VideoBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@video+block@video_5feb0a6c6f49" data-block-type="video" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Video"}
</script>
<h3 class="hd hd-2">Video</h3>
<div
id="video_video_5feb0a6c6f49"
class="video closed"
data-metadata='{"transcriptLanguages": {"en": "English"}, "lmsRootURL": "https://openlearninglibrary.mit.edu", "captionDataDir": null, "ytTestTimeout": 1500, "saveStateEnabled": false, "start": 0.0, "autoAdvance": false, "ytApiUrl": "https://www.youtube.com/iframe_api", "ytMetadataEndpoint": "", "recordedYoutubeIsAvailable": true, "speed": null, "generalSpeed": 1.0, "streams": "1.00:gnv4ikbl_Uo", "completionEnabled": false, "end": 0.0, "transcriptTranslationUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_5feb0a6c6f49/handler/transcript/translation/__lang__", "prioritizeHls": false, "duration": 545.47, "publishCompletionUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_5feb0a6c6f49/handler/publish_completion", "completionPercentage": 0.95, "transcriptAvailableTranslationsUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_5feb0a6c6f49/handler/transcript/available_translations", "showCaptions": "true", "saveStateUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_5feb0a6c6f49/handler/xmodule_handler/save_user_state", "poster": null, "autoplay": false, "transcriptLanguage": "en", "autohideHtml5": false, "savedVideoPosition": 0.0, "sources": ["https://d2f1egay8yehza.cloudfront.net/MIT600512016-V003400_DTH.mp4", "https://d2f1egay8yehza.cloudfront.net/MIT600512016-V003400/MIT600512016-V003400.m3u8"]}'
data-bumper-metadata='null'
data-autoadvance-enabled="False"
data-poster='null'
tabindex="-1"
>
<div class="focus_grabber first"></div>
<div class="tc-wrapper">
<div class="video-wrapper">
<span tabindex="0" class="spinner" aria-hidden="false" aria-label="Loading video player"></span>
<span tabindex="-1" class="btn-play fa fa-youtube-play fa-2x is-hidden" aria-hidden="true" aria-label="Play video"></span>
<div class="video-player-pre"></div>
<div class="video-player">
<div id="video_5feb0a6c6f49"></div>
<h4 class="hd hd-4 video-error is-hidden">No playable video sources found.</h4>
<h4 class="hd hd-4 video-hls-error is-hidden">
Your browser does not support this video format. Try using a different browser.
</h4>
</div>
<div class="video-player-post"></div>
<div class="closed-captions"></div>
<div class="video-controls is-hidden">
<div>
<div class="vcr"><div class="vidtime">0:00 / 0:00</div></div>
<div class="secondary-controls"></div>
</div>
</div>
</div>
</div>
<div class="focus_grabber last"></div>
<h3 class="hd hd-4 downloads-heading sr" id="video-download-transcripts_video_5feb0a6c6f49">Downloads and transcripts</h3>
<div class="wrapper-downloads" role="region" aria-labelledby="video-download-transcripts_video_5feb0a6c6f49">
<div class="wrapper-download-transcripts">
<h4 class="hd hd-5">Transcripts</h4>
<ul class="list-download-transcripts">
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_5feb0a6c6f49/handler/transcript/download" data-value="srt">Download SubRip (.srt) file</a>
</li>
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_5feb0a6c6f49/handler/transcript/download" data-value="txt">Download Text (.txt) file</a>
</li>
</ul>
</div>
</div>
</div>
</div>
</div>
<div class="vert vert-1" data-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_1f9920bdd71e">
<div class="xblock xblock-public_view xblock-public_view-html xmodule_display xmodule_HtmlBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_1f9920bdd71e" data-block-type="html" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "HTMLModule"}
</script>
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<h2 id="stronger_vs_weaker_specs">Stronger vs. weaker specs</h2>
<div data-outline="stronger_vs_weaker_specs">
<p>Suppose you want to change a method — either how its implementation behaves, or the specification itself. There are already clients that depend on the method's current specification. How do you compare the behaviors of two specifications to decide whether it's safe to replace the old spec with the new spec?</p>
<p>A specification S2 is stronger than or equal to a specification S1 if</p>
<ul>
<li>S2's precondition is weaker than or equal to S1's,
<br> and
</li>
<li>S2's postcondition is stronger than or equal to S1's for the states that satisfy S1's precondition.</li>
</ul>
<p>If this is the case, then an implementation that satisfies S2 can be used to satisfy S1 as well, and it's safe to replace S1 with S2 in your program.</p>
<p>These two rules embody several ideas. They tell you that you can always weaken the precondition; placing fewer demands on a client will never upset them. And you can always strengthen the post-condition, which means making more promises.</p>
<p>For example, this spec for <code>find</code>:</p><pre class="no-markdown">static int find<sub>ExactlyOne</sub>(int[] a, int val)
<em>requires</em>: val occurs <strong>exactly once</strong> in a
<em>effects</em>: returns index i such that a[i] = val
</pre>
<p>can be replaced with:</p><pre class="no-markdown">static int find<sub>OneOrMore,AnyIndex</sub>(int[] a, int val)
<em>requires</em>: val occurs <strong>at least once</strong> in a
<em>effects</em>: returns index i such that a[i] = val
</pre>
<p>which has a weaker precondition. This in turn can be replaced with:</p><pre class="no-markdown">static int find<sub>OneOrMore,FirstIndex</sub>(int[] a, int val)
<em>requires</em>: val occurs <strong>at least once</strong> in a
<em>effects</em>: returns <strong>lowest</strong> index i such that a[i] = val
</pre>
<p>which has a stronger postcondition. </p>
<p>What about this specification:</p><pre class="no-markdown">static int find<sub>CanBeMissing</sub>(int[] a, int val)
<em>requires</em>: <strong>nothing</strong>
<em>effects</em>: returns index i such that a[i] = val,
<strong>or -1 if no such i</strong>
</pre>
<p>We'll come back to <code class="no-markdown">find<sub>CanBeMissing</sub></code> in the exercises.</p>
</div>
<h2 id="diagramming_specifications">Diagramming specifications</h2>
<div data-outline="diagramming_specifications">
<p>Imagine (very abstractly) the space of all possible Java methods.</p>
<p>Each point in this space represents a method implementation.</p>
<p>First we'll diagram the <code class="no-markdown">find<sub>First</sub></code> and <code class="no-markdown">find<sub>Last</sub></code> implementations we saw earlier:</p>
<pre class="no-markdown"><code>static int find<sub>First</sub>(int[] arr, int val) {
for (int i = 0; i < arr.length; i++) {
if (arr[i] == val) return i;
}
return arr.length;
}
</code></pre><pre class="no-markdown"><code>static int find<sub>Last</sub>(int[] arr, int val) {
for (int i = arr.length - 1 ; i >= 0; i--) {
if (arr[i] == val) return i;
}
return -1;
}
</code></pre>
<div class="panel panel-default panel-figure pull-right pull-margin">
<object data="/assets/courseware/v1/4f2c125c7c3e0b62ef3d59802b46d1c0/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-space1.svg"></object>
</div>
<p>Notice that <code class="no-markdown">find<sub>First</sub></code> and <code class="no-markdown">find<sub>Last</sub></code> are <em>not specs</em>. They are implementations, with method bodies that implement their actual behavior. So we denote them as points in the space.</p><span class="clearfix"></span>
<div class="panel panel-default panel-figure pull-right pull-margin">
<object data="/assets/courseware/v1/2e3a2fa5bdebc6c79c68b7ac3f0a1f02/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-space2.svg"></object>
</div>
<p>A specification defines a <em>region</em> in the space of all possible implementations. A given implementation either behaves according to the spec, satisfying the precondition-implies-postcondition contract (it is inside the region), or it does not (outside the region).</p>
<p>Both <code class="no-markdown">find<sub>First</sub></code> and <code class="no-markdown">find<sub>Last</sub></code> satisfy <code class="no-markdown">find<sub>OneOrMore,AnyIndex</sub></code>, so they are inside the region defined by that spec.</p><span class="clearfix"></span>
<p>We can imagine clients looking in on this space: the specification acts as a firewall.</p>
<ul>
<li>
<p>Implementors have the freedom to move around inside the spec, changing their code without fear of upsetting a client. This is crucial in order for the implementor to be able to improve the performance of their algorithm, the clarity of their code, or to change their approach when they discover a bug, etc.</p>
</li>
<li>
<p>Clients don't know which implementation they will get. They must respect the spec, but also have the freedom to change how they're using the implementation without fear that it will suddenly break.</p>
</li>
</ul>
<div class="panel panel-default panel-figure pull-right pull-margin">
<object data="/assets/courseware/v1/734a00f02a3b2be2f63a7aa66d3d2463/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-space-s1s2.svg"></object>
</div>
<p>How will similar specifications relate to one another? Suppose we start with specification S1 and adapt it to create a new specification S2.</p>
<p>If S2 is stronger than S1, how will these specs appear in our diagram?</p>
<ul>
<li>
<p>Let's start by <strong>strengthening the postcondition</strong>. If S2's postcondition is now stronger than S1's postcondition, then S2 is the stronger specification. Think about what strengthening the postcondition means for implementors. It means they have less freedom, because the requirements on their output are stronger.</p>
</li>
<li>
<p>If we <strong>weaken the precondition</strong>, which again makes S2 a stronger specification, then implementations will have to handle new inputs that were previously excluded by the spec. If they behaved badly on those inputs before, we wouldn't have noticed, but now their bad behavior is exposed.</p>
</li>
</ul>
<p>So when S2 is stronger than S1, it defines a <em>smaller</em> region in this diagram. Fewer implementations satisfy S2 than S1. Every implementation that satisfies S2 also satisfies S1, though, so the smaller region S2 is nested inside S1.</p>
<div class="panel panel-default panel-figure pull-right pull-margin">
<object data="/assets/courseware/v1/4315fbaad6fa4d26fbc950bc0f97a0a0/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-space3.svg"></object>
</div>
<p>Now let's see how this works with our find specifications. Where does <code class="no-markdown">find<sub>OneOrMore,FirstIndex</sub></code> fit on the diagram? Is it stronger or weaker? Implementations can satisfy <code class="no-markdown">find<sub>OneOrMore,AnyIndex</sub></code> by returning any index <code>i</code>, but now the spec demands the <em>lowest</em> index <code>i</code>. So there are now implementations <em>inside</em> <code class="no-markdown">find<sub>OneOrMore,AnyIndex</sub></code> but <em>outside</em> <code class="no-markdown">find<sub>OneOrMore,FirstIndex</sub></code>.</p>
<p>Could there be implementations <em>inside</em> <code class="no-markdown">find<sub>OneOrMore,FirstIndex</sub></code> but <em>outside</em> <code class="no-markdown">find<sub>OneOrMore,AnyIndex</sub></code>? No. All of those implementations satisfy a stronger postcondition than what <code class="no-markdown">find<sub>OneOrMore,AnyIndex</sub></code> demands.</p>
<p>In our figure, since <code class="no-markdown">find<sub>Last</sub></code> iterates from the end of the array <code>arr</code>, it does not satisfy <code class="no-markdown">find<sub>OneOrMore,FirstIndex</sub></code> and is outside that region.<span class="clearfix"></span></p>
<p>Another specification S3 that is neither stronger nor weaker than S1 might overlap (such that there exist implementations that satisfy only S1, only S3, and both S1 and S3) or might be disjoint. In both cases, S1 and S3 are incomparable.</p>
</div>
</div>
</div>
</div>
</div>
<div class="xblock xblock-public_view xblock-public_view-vertical" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@vertical+block@vertical_Questions_d5c1b1f0d583" data-block-type="vertical" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">Questions</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_fff67ba8819a">
<div class="xblock xblock-public_view xblock-public_view-html xmodule_display xmodule_HtmlBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_fff67ba8819a" data-block-type="html" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "HTMLModule"}
</script>
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<script src="/assets/courseware/v1/3e6443fb95285d2dc06e8ffc448b9bdf/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism.js"></script>
<script src="/assets/courseware/v1/2ba76f8bdfef4e2d45e31a3dc5208470/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/edx-script-v1.js"></script>
</div>
</div>
<div class="vert vert-1" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-bulking-up">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-bulking-up" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-bulking-up" class="problems-wrapper" role="group"
aria-labelledby="05-bulking-up-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-bulking-up" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-bulking-up/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-bulking-up-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-bulking-up-problem-progress" tabindex="-1">
bulking up
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-bulking-up-problem-progress"></div>
<div class="problem">
<div>
<p>When a specification is strengthened (check all that apply):</p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-bulking-up_2_1">
<fieldset aria-describedby="status_05-bulking-up_2_1">
<div class="field">
<input type="checkbox" name="input_05-bulking-up_2_1[]" id="input_05-bulking-up_2_1_choice_0" class="field-input input-checkbox" value="choice_0"/><label id="05-bulking-up_2_1-choice_0-label" for="input_05-bulking-up_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-bulking-up_2_1"> fewer implementations satisfy it
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-bulking-up_2_1[]" id="input_05-bulking-up_2_1_choice_1" class="field-input input-checkbox" value="choice_1"/><label id="05-bulking-up_2_1-choice_1-label" for="input_05-bulking-up_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-bulking-up_2_1"> more implementations satisfy it
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-bulking-up_2_1[]" id="input_05-bulking-up_2_1_choice_2" class="field-input input-checkbox" value="choice_2"/><label id="05-bulking-up_2_1-choice_2-label" for="input_05-bulking-up_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-bulking-up_2_1"> fewer clients can use it
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-bulking-up_2_1[]" id="input_05-bulking-up_2_1_choice_3" class="field-input input-checkbox" value="choice_3"/><label id="05-bulking-up_2_1-choice_3-label" for="input_05-bulking-up_2_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-bulking-up_2_1"> more clients can use it
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-bulking-up_2_1[]" id="input_05-bulking-up_2_1_choice_4" class="field-input input-checkbox" value="choice_4"/><label id="05-bulking-up_2_1-choice_4-label" for="input_05-bulking-up_2_1_choice_4" class="response-label field-label label-inline" aria-describedby="status_05-bulking-up_2_1"> none of the above
</label>
</div>
<span id="answer_05-bulking-up_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-bulking-up_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-bulking-up_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="bulking up" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-bulking-up" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-bulking-up">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-bulking-up-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-bulking-up-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-bulking-up-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-2" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-strength-is-truth">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-strength-is-truth" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-strength-is-truth" class="problems-wrapper" role="group"
aria-labelledby="05-strength-is-truth-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-strength-is-truth" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-strength-is-truth/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-strength-is-truth-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-strength-is-truth-problem-progress" tabindex="-1">
strength is truth
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-strength-is-truth-problem-progress"></div>
<div class="problem">
<div>
<p>Which of the following can be true about a pair of specifications <em>A</em> and <em>B</em>? Check all that apply.</p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-strength-is-truth_2_1">
<fieldset aria-describedby="status_05-strength-is-truth_2_1">
<div class="field">
<input type="checkbox" name="input_05-strength-is-truth_2_1[]" id="input_05-strength-is-truth_2_1_choice_0" class="field-input input-checkbox" value="choice_0"/><label id="05-strength-is-truth_2_1-choice_0-label" for="input_05-strength-is-truth_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-strength-is-truth_2_1"> 1. <em>A</em> can be stronger than <em>B</em> and have a weaker precondition
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-strength-is-truth_2_1[]" id="input_05-strength-is-truth_2_1_choice_1" class="field-input input-checkbox" value="choice_1"/><label id="05-strength-is-truth_2_1-choice_1-label" for="input_05-strength-is-truth_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-strength-is-truth_2_1"> 2. <em>A</em> can be stronger than <em>B</em> and have the same precondition
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-strength-is-truth_2_1[]" id="input_05-strength-is-truth_2_1_choice_2" class="field-input input-checkbox" value="choice_2"/><label id="05-strength-is-truth_2_1-choice_2-label" for="input_05-strength-is-truth_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-strength-is-truth_2_1"> 3. <em>A</em> can be stronger than <em>B</em> and have a stronger precondition
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-strength-is-truth_2_1[]" id="input_05-strength-is-truth_2_1_choice_3" class="field-input input-checkbox" value="choice_3"/><label id="05-strength-is-truth_2_1-choice_3-label" for="input_05-strength-is-truth_2_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-strength-is-truth_2_1"> 4. <em>A</em> can be stronger than <em>B</em> and have an incomparable precondition
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-strength-is-truth_2_1[]" id="input_05-strength-is-truth_2_1_choice_4" class="field-input input-checkbox" value="choice_4"/><label id="05-strength-is-truth_2_1-choice_4-label" for="input_05-strength-is-truth_2_1_choice_4" class="response-label field-label label-inline" aria-describedby="status_05-strength-is-truth_2_1"> 5. <em>A</em> can be incomparable to <em>B</em>
</label>
</div>
<span id="answer_05-strength-is-truth_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-strength-is-truth_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-strength-is-truth_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="strength is truth" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-strength-is-truth" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-strength-is-truth">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-strength-is-truth-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-strength-is-truth-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-strength-is-truth-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-3" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-finding-find1">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-finding-find1" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-finding-find1" class="problems-wrapper" role="group"
aria-labelledby="05-finding-find1-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-finding-find1" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-finding-find1/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-finding-find1-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-finding-find1-problem-progress" tabindex="-1">
finding find1
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-finding-find1-problem-progress"></div>
<div class="problem">
<div>
<p>Here are the <em>find</em> specifications from the reading:</p>
<pre class="code">
static int find1(int[] a, int val)
requires: val occurs exactly once in a
effects: returns index i such that a[i] = val
</pre>
<pre class="code">
static int findStronger2(int[] a, int val)
requires: val occurs at least once in a
effects: returns index i such that a[i] = val
</pre>
<pre class="code">
static int findStronger3(int[] a, int val)
requires: val occurs at least once in a
effects: returns lowest index i such that a[i] = val
</pre>
<pre class="code">
static int find4(int[] a, int val)
requires: nothing
effects: returns index i such that a[i] = val,
or -1 if no such i
</pre>
<p>We already know that <em>findStronger3</em> is stronger than <em>findStronger2</em>, which is stronger than <em>find1</em>.</p>
<img src="/assets/courseware/v1/f0ebea0328cfc920e4c74b12996a7af9/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-findStronger2-3.svg"/>
<p>Where is <em>find1</em> on the diagram?</p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-finding-find1_2_1">
<fieldset aria-describedby="status_05-finding-find1_2_1">
<div class="field">
<input type="radio" name="input_05-finding-find1_2_1" id="input_05-finding-find1_2_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-finding-find1_2_1-choice_0-label" for="input_05-finding-find1_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-finding-find1_2_1">
<img src="/assets/courseware/v1/cb6cd5612c66c29c121936d18151f7d1/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-find1-small.svg"/>
</label>
</div>
<div class="field">
<input type="radio" name="input_05-finding-find1_2_1" id="input_05-finding-find1_2_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-finding-find1_2_1-choice_1-label" for="input_05-finding-find1_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-finding-find1_2_1">
<img src="/assets/courseware/v1/611792625c25ead53778da577e7e8331/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-find1-between.svg"/>
</label>
</div>
<div class="field">
<input type="radio" name="input_05-finding-find1_2_1" id="input_05-finding-find1_2_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-finding-find1_2_1-choice_2-label" for="input_05-finding-find1_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-finding-find1_2_1">
<img src="/assets/courseware/v1/9c0ee02b68edd4d883fea7d5f7b41d6c/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-find1-large.svg"/>
</label>
</div>
<div class="field">
<input type="radio" name="input_05-finding-find1_2_1" id="input_05-finding-find1_2_1_choice_3" class="field-input input-radio" value="choice_3"/><label id="05-finding-find1_2_1-choice_3-label" for="input_05-finding-find1_2_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-finding-find1_2_1">
<img src="/assets/courseware/v1/f46ce68aa9cc2cec7a05ba6641116ebe/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-find1-outside.svg"/>
</label>
</div>
<span id="answer_05-finding-find1_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-finding-find1_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-finding-find1_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="finding find1" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-finding-find1" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-finding-find1">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-finding-find1-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-finding-find1-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-finding-find1-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-4" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-finding-find4">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-finding-find4" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-finding-find4" class="problems-wrapper" role="group"
aria-labelledby="05-finding-find4-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-finding-find4" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-finding-find4/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-finding-find4-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-finding-find4-problem-progress" tabindex="-1">
finding find4
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-finding-find4-problem-progress"></div>
<div class="problem">
<div>
<p>Let's determine where <em>find4</em> is on the diagram.</p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-finding-find4_2_1">
<fieldset aria-describedby="status_05-finding-find4_2_1">
<legend id="05-finding-find4_2_1-legend" class="response-fieldset-legend field-group-hd">How does find1 compare to find4?</legend>
<div class="field">
<input type="radio" name="input_05-finding-find4_2_1" id="input_05-finding-find4_2_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-finding-find4_2_1-choice_0-label" for="input_05-finding-find4_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-finding-find4_2_1"> find4 is weaker
</label>
</div>
<div class="field">
<input type="radio" name="input_05-finding-find4_2_1" id="input_05-finding-find4_2_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-finding-find4_2_1-choice_1-label" for="input_05-finding-find4_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-finding-find4_2_1"> find4 is stronger
</label>
</div>
<div class="field">
<input type="radio" name="input_05-finding-find4_2_1" id="input_05-finding-find4_2_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-finding-find4_2_1-choice_2-label" for="input_05-finding-find4_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-finding-find4_2_1"> find4 and find1 are incomparable
</label>
</div>
<span id="answer_05-finding-find4_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-finding-find4_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-finding-find4_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="finding find4" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-finding-find4" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-finding-find4">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-finding-find4-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-finding-find4-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-finding-find4-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-5" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-vs-findstronger2">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-vs-findstronger2" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-vs-findstronger2" class="problems-wrapper" role="group"
aria-labelledby="05-vs-findstronger2-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-vs-findstronger2" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-vs-findstronger2/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-vs-findstronger2-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-vs-findstronger2-problem-progress" tabindex="-1">
vs. findStronger2
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-vs-findstronger2-problem-progress"></div>
<div class="problem">
<div>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-vs-findstronger2_2_1">
<fieldset aria-describedby="status_05-vs-findstronger2_2_1">
<legend id="05-vs-findstronger2_2_1-legend" class="response-fieldset-legend field-group-hd">How does findStronger2 compare to find4?</legend>
<div class="field">
<input type="radio" name="input_05-vs-findstronger2_2_1" id="input_05-vs-findstronger2_2_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-vs-findstronger2_2_1-choice_0-label" for="input_05-vs-findstronger2_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-vs-findstronger2_2_1"> find4 is weaker
</label>
</div>
<div class="field">
<input type="radio" name="input_05-vs-findstronger2_2_1" id="input_05-vs-findstronger2_2_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-vs-findstronger2_2_1-choice_1-label" for="input_05-vs-findstronger2_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-vs-findstronger2_2_1"> find4 is stronger
</label>
</div>
<div class="field">
<input type="radio" name="input_05-vs-findstronger2_2_1" id="input_05-vs-findstronger2_2_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-vs-findstronger2_2_1-choice_2-label" for="input_05-vs-findstronger2_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-vs-findstronger2_2_1"> find4 and findStronger2 are incomparable
</label>
</div>
<span id="answer_05-vs-findstronger2_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-vs-findstronger2_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-vs-findstronger2_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="vs. findStronger2" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-vs-findstronger2" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-vs-findstronger2">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-vs-findstronger2-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-vs-findstronger2-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-vs-findstronger2-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-6" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-vs-findstronger3">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-vs-findstronger3" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-vs-findstronger3" class="problems-wrapper" role="group"
aria-labelledby="05-vs-findstronger3-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-vs-findstronger3" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-vs-findstronger3/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-vs-findstronger3-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-vs-findstronger3-problem-progress" tabindex="-1">
vs. findStronger3
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-vs-findstronger3-problem-progress"></div>
<div class="problem">
<div>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-vs-findstronger3_2_1">
<fieldset aria-describedby="status_05-vs-findstronger3_2_1">
<legend id="05-vs-findstronger3_2_1-legend" class="response-fieldset-legend field-group-hd">How does findStronger3 compare to find4?</legend>
<div class="field">
<input type="radio" name="input_05-vs-findstronger3_2_1" id="input_05-vs-findstronger3_2_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-vs-findstronger3_2_1-choice_0-label" for="input_05-vs-findstronger3_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-vs-findstronger3_2_1"> find4 is weaker
</label>
</div>
<div class="field">
<input type="radio" name="input_05-vs-findstronger3_2_1" id="input_05-vs-findstronger3_2_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-vs-findstronger3_2_1-choice_1-label" for="input_05-vs-findstronger3_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-vs-findstronger3_2_1"> find4 is stronger
</label>
</div>
<div class="field">
<input type="radio" name="input_05-vs-findstronger3_2_1" id="input_05-vs-findstronger3_2_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-vs-findstronger3_2_1-choice_2-label" for="input_05-vs-findstronger3_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-vs-findstronger3_2_1"> find4 and findStronger3 are incomparable
</label>
</div>
<span id="answer_05-vs-findstronger3_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-vs-findstronger3_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-vs-findstronger3_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="vs. findStronger3" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-vs-findstronger3" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-vs-findstronger3">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-vs-findstronger3-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-vs-findstronger3-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-vs-findstronger3-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-7" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-found">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-found" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-found" class="problems-wrapper" role="group"
aria-labelledby="05-found-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-found" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-found/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-found-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-found-problem-progress" tabindex="-1">
found
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-found-problem-progress"></div>
<div class="problem">
<div>
<img src="/assets/courseware/v1/f0ebea0328cfc920e4c74b12996a7af9/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-findStronger2-3.svg"/>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-found_2_1">
<fieldset aria-describedby="status_05-found_2_1">
<legend id="05-found_2_1-legend" class="response-fieldset-legend field-group-hd">Where is find4 on the diagram?</legend>
<div class="field">
<input type="radio" name="input_05-found_2_1" id="input_05-found_2_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-found_2_1-choice_0-label" for="input_05-found_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-found_2_1">
<img src="/assets/courseware/v1/5db26211a2a4e915ad1a96d887a1a07c/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-find4-small.svg"/>
</label>
</div>
<div class="field">
<input type="radio" name="input_05-found_2_1" id="input_05-found_2_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-found_2_1-choice_1-label" for="input_05-found_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-found_2_1">
<img src="/assets/courseware/v1/a9c585e25634b96c23882029ff5c9e2e/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-find4-overlap2.svg"/>
</label>
</div>
<div class="field">
<input type="radio" name="input_05-found_2_1" id="input_05-found_2_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-found_2_1-choice_2-label" for="input_05-found_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-found_2_1">
<img src="/assets/courseware/v1/8b83b35c90f147829cfb31930b267f43/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-find4-overlap23.svg"/>
</label>
</div>
<div class="field">
<input type="radio" name="input_05-found_2_1" id="input_05-found_2_1_choice_3" class="field-input input-radio" value="choice_3"/><label id="05-found_2_1-choice_3-label" for="input_05-found_2_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-found_2_1">
<img src="/assets/courseware/v1/50775675ccc5434a7f0c1c9b90d390da/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-find4-overlap3.svg"/>
</label>
</div>
<div class="field">
<input type="radio" name="input_05-found_2_1" id="input_05-found_2_1_choice_4" class="field-input input-radio" value="choice_4"/><label id="05-found_2_1-choice_4-label" for="input_05-found_2_1_choice_4" class="response-label field-label label-inline" aria-describedby="status_05-found_2_1">
<img src="/assets/courseware/v1/a3efa3190c1a71f59e0c6aada09472ea/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/05-find4-outside.svg"/>
</label>
</div>
<span id="answer_05-found_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-found_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-found_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="found" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-found" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-found">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-found-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-found-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-found-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
</div>
</div>
<div class="xblock xblock-public_view xblock-public_view-vertical" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@vertical+block@Designing_Good_Specifications" data-block-type="vertical" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">Designing Good Specifications</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+6.005.1x+3T2016+type@video+block@video_1a248dd761c4">
<div class="xblock xblock-public_view xblock-public_view-video xmodule_display xmodule_VideoBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@video+block@video_1a248dd761c4" data-block-type="video" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Video"}
</script>
<h3 class="hd hd-2">Video</h3>
<div
id="video_video_1a248dd761c4"
class="video closed"
data-metadata='{"transcriptLanguages": {"en": "English"}, "lmsRootURL": "https://openlearninglibrary.mit.edu", "captionDataDir": null, "ytTestTimeout": 1500, "saveStateEnabled": false, "start": 0.0, "autoAdvance": false, "ytApiUrl": "https://www.youtube.com/iframe_api", "ytMetadataEndpoint": "", "recordedYoutubeIsAvailable": true, "speed": null, "generalSpeed": 1.0, "streams": "1.00:h-N1FiBuvAA", "completionEnabled": false, "end": 0.0, "transcriptTranslationUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_1a248dd761c4/handler/transcript/translation/__lang__", "prioritizeHls": false, "duration": 756.48, "publishCompletionUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_1a248dd761c4/handler/publish_completion", "completionPercentage": 0.95, "transcriptAvailableTranslationsUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_1a248dd761c4/handler/transcript/available_translations", "showCaptions": "true", "saveStateUrl": "/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_1a248dd761c4/handler/xmodule_handler/save_user_state", "poster": null, "autoplay": false, "transcriptLanguage": "en", "autohideHtml5": false, "savedVideoPosition": 0.0, "sources": ["https://d2f1egay8yehza.cloudfront.net/MIT600512016-V003300_DTH.mp4", "https://d2f1egay8yehza.cloudfront.net/MIT600512016-V003300/MIT600512016-V003300.m3u8"]}'
data-bumper-metadata='null'
data-autoadvance-enabled="False"
data-poster='null'
tabindex="-1"
>
<div class="focus_grabber first"></div>
<div class="tc-wrapper">
<div class="video-wrapper">
<span tabindex="0" class="spinner" aria-hidden="false" aria-label="Loading video player"></span>
<span tabindex="-1" class="btn-play fa fa-youtube-play fa-2x is-hidden" aria-hidden="true" aria-label="Play video"></span>
<div class="video-player-pre"></div>
<div class="video-player">
<div id="video_1a248dd761c4"></div>
<h4 class="hd hd-4 video-error is-hidden">No playable video sources found.</h4>
<h4 class="hd hd-4 video-hls-error is-hidden">
Your browser does not support this video format. Try using a different browser.
</h4>
</div>
<div class="video-player-post"></div>
<div class="closed-captions"></div>
<div class="video-controls is-hidden">
<div>
<div class="vcr"><div class="vidtime">0:00 / 0:00</div></div>
<div class="secondary-controls"></div>
</div>
</div>
</div>
</div>
<div class="focus_grabber last"></div>
<h3 class="hd hd-4 downloads-heading sr" id="video-download-transcripts_video_1a248dd761c4">Downloads and transcripts</h3>
<div class="wrapper-downloads" role="region" aria-labelledby="video-download-transcripts_video_1a248dd761c4">
<div class="wrapper-download-transcripts">
<h4 class="hd hd-5">Transcripts</h4>
<ul class="list-download-transcripts">
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_1a248dd761c4/handler/transcript/download" data-value="srt">Download SubRip (.srt) file</a>
</li>
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@video+block@video_1a248dd761c4/handler/transcript/download" data-value="txt">Download Text (.txt) file</a>
</li>
</ul>
</div>
</div>
</div>
</div>
</div>
<div class="vert vert-1" data-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_4d7f368259ed">
<div class="xblock xblock-public_view xblock-public_view-html xmodule_display xmodule_HtmlBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_4d7f368259ed" data-block-type="html" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "HTMLModule"}
</script>
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<h2 id="designing_good_specifications">Designing good specifications</h2>
<div data-outline="designing_good_specifications">
<p>What makes a good method? Designing a method means primarily writing a specification.</p>
<p>About the form of the specification: it should obviously be succinct, clear, and well-structured, so that it's easy to read.</p>
<p>The content of the specification, however, is harder to prescribe. There are no infallible rules, but there are some useful guidelines.</p>
<h3 id="the_specification_should_be_coherent">The specification should be coherent</h3>
<div data-outline="the_specification_should_be_coherent">
<p>The spec shouldn't have lots of different cases. Long argument lists, deeply nested if-statements, and boolean flags are all signs of trouble. Consider this specification:</p><pre class="no-markdown">static int sumFind(int[] a, int[] b, int val)
<em>effects</em>: returns the sum of all indices in arrays a and b at which
val appears
</pre>
<p>Is this a well-designed procedure? Probably not: it's incoherent, since it does several things (finding in two arrays and summing the indexes) that are not really related. It would be better to use two separate procedures, one that finds the indexes, and the other that sums them.</p>
<p>Here's another example, <a href="/courses/course-v1:MITx+6.005.1x+3T2016/jump_to_id/vertical-dont-use-global-variables#smelly_example_3">the <code>countLongWords</code> method from <em>Code Review</em></a>:</p><pre><code class="language-java hljs"><span class="hljs-keyword">public</span> <span class="hljs-keyword">static</span> <span class="hljs-keyword">int</span> LONG_WORD_LENGTH = <span class="hljs-number">5</span>;
<span class="hljs-keyword">public</span> <span class="hljs-keyword">static</span> String longestWord;
<span class="hljs-comment handout-javadoc-comment">/**
* Update longestWord to be the longest element of words, and print
* the number of elements with length > LONG_WORD_LENGTH to the console.
* <span class="hljs-doctag">@param</span> words list to search for long words
*/</span>
<span class="hljs-function"><span class="hljs-keyword">public</span> <span class="hljs-keyword">static</span> <span class="hljs-keyword">void</span> <span class="hljs-title">countLongWords</span><span class="hljs-params">(List<String> words)</span></span></code></pre>
<p>In addition to <a href="/courses/course-v1:MITx+6.005.1x+3T2016/jump_to_id/vertical-dont-use-global-variables#dont_use_global_variables">terrible use of global variables</a> and <a href="/courses/course-v1:MITx+6.005.1x+3T2016/jump_to_id/vertical-dont-use-global-variables#methods_should_return_results_not_print_them">printing instead of returning</a>, the specification is not coherent — it does two different things, counting words and finding the longest word.</p>
<p>Separating those two responsibilities into two different methods will make them simpler (easy to understand) and more useful in other contexts (ready for change).</p>
</div>
<h3 id="the_results_of_a_call_should_be_informative">The results of a call should be informative</h3>
<div data-outline="the_results_of_a_call_should_be_informative">
<p>Consider the specification of a method that puts a value in a map, where keys are of some type <code>K</code> and values are of some type <code>V</code>:</p>
<pre class="no-markdown">static V put (Map<K,V> map, K key, V val)
<em>requires</em>: val may be null, and map may contain null values
<em>effects</em>: inserts (key, val) into the mapping,
overriding any existing mapping for key, and
returns old value for key, unless none,
in which case it returns null
</pre>
<p>Note that the precondition does not rule out <code>null</code> values so the map can store <code>null</code>s. But the postcondition uses <code>null</code> as a special return value for a missing key. This means that if <code>null</code> is returned, you can't tell whether the key was not bound previously, or whether it was in fact bound to <code>null</code>. This is not a very good design, because the return value is useless unless you know for sure that you didn't insert <code>null</code>s.</p>
</div>
<h3 id="the_specification_should_be_strong_enough">The specification should be strong enough</h3>
<div data-outline="the_specification_should_be_strong_enough">
<p>Of course the spec should give clients a strong enough guarantee in the general case — it needs to satisfy their basic requirements. We must use extra care when specifying the special cases, to make sure they don't undermine what would otherwise be a useful method.</p>
<p>For example, there's no point throwing an exception for a bad argument but allowing arbitrary mutations, because a client won't be able to determine what mutations have actually been made. Here's a specification illustrating this flaw (and also written in an inappropriately operational style):</p><pre class="no-markdown">static void addAll(List<T> list1, List<T> list2)
<em>effects</em>: adds the elements of list2 to list1,
unless it encounters a null element,
at which point it throws a NullPointerException
</pre>
<p>If a <code>NullPointerException</code> is thrown, the client is left to figure out on their own which elements of <code>list2</code> actually made it to <code>list1</code>.</p>
</div>
<h3 id="the_specification_should_also_be_weak_enough">The specification should also be weak enough</h3>
<div data-outline="the_specification_should_also_be_weak_enough">
<p>Consider this specification for a method that opens a file:</p><pre class="no-markdown">static File open(String filename)
<em>effects</em>: opens a file named filename
</pre>
<p>This is a bad specification. It lacks important details: is the file opened for reading or writing? Does it already exist or is it created? And it's too strong, since there's no way it can guarantee to open a file. The process in which it runs may lack permission to open a file, or there might be some problem with the file system beyond the control of the program. Instead, the specification should say something much weaker: that it attempts to open a file, and if it succeeds, the file has certain properties.</p>
</div>
<h3 id="the_specification_should_use_abstract_types_where_possible">The specification should use <em>abstract types</em> where possible</h3>
<div data-outline="the_specification_should_use_abstract_types_where_possible">
<p>In Java, we can distinguish between more abstract notions like a <code>List</code> or <code>Set</code> and particular implementations like <code>ArrayList</code> or <code>HashSet</code>.</p>
<p>Writing our specification with <em>abstract types</em> gives more freedom to both the client and the implementor. In Java, this often means using an interface type, like <code>Map</code> or <code>Reader</code>, instead of specific implementation types like <code>HashMap</code> or <code>FileReader</code>. Consider this specification:</p><pre class="no-markdown">static ArrayList<T> reverse(ArrayList<T> list)
<em>effects</em>: returns a new list which is the reversal of list, i.e.
newList[i] == list[n-i-1]
for all 0 <= i < n, where n = list.size()
</pre>
<p>This forces the client to pass in an <code>ArrayList</code>, and forces the implementor to return an <code>ArrayList</code>, even if there might be alternative <code>List</code> implementations that they would rather use. Since the behavior of the specification doesn't depend on anything specific about <code>ArrayList</code>, it would be better to write this spec in terms of the more abstract <code>List</code>.</p>
</div>
</div>
<h2 id="precondition_or_postcondition">Precondition or postcondition?</h2>
<div data-outline="precondition_or_postcondition">
<p>Another design issue is whether to use a precondition, and if so, whether the method code should attempt to make sure the precondition has been met before proceeding. In fact, the most common use of preconditions is to demand a property precisely because it would be hard or expensive for the method to check it.</p>
<p>As mentioned above, a non-trivial precondition inconveniences clients, because they have to ensure that they don't call the method in a bad state (that violates the precondition); if they do, there is no predictable way to recover from the error. So users of methods don't like preconditions. That's why the Java API classes, for example, tend to specify (as a postcondition) that they throw unchecked exceptions when arguments are inappropriate. This approach makes it easier to find the bug or incorrect assumption in the caller code that led to passing bad arguments. In general, it's better to <strong>fail fast</strong>, as close as possible to the site of the bug, rather than let bad values propagate through a program far from their original cause.</p>
<p>Sometimes, it's not feasible to check a condition without making a method unacceptably slow, and a precondition is often necessary in this case. If we wanted to implement the <code>find</code> method using binary search, we would have to require that the array be sorted. Forcing the method to actually <em>check</em> that the array is sorted would defeat the entire purpose of the binary search: to obtain a result in logarithmic and not linear time.</p>
<p>The decision of whether to use a precondition is an engineering judgment. The key factors are the cost of the check (in writing and executing code), and the scope of the method. If it's only called locally in a class, the precondition can be discharged by carefully checking all the sites that call the method. But if the method is public, and used by other developers, it would be less wise to use a precondition. Instead, like the Java API classes, you should throw an exception.</p>
</div>
<h2 id="about_access_control">About access control</h2>
<div data-outline="about_access_control">
<!--
<div class="handout-solo alert alert-warning">
<p>Read: <strong><a href="http://docs.oracle.com/javase/tutorial/java/package/index.html" class="alert-link">Packages</a></strong> (7 short pages) in the Java Tutorials.</p>
</div>
<div class="handout-solo alert alert-warning">
<p>Read: <strong><a href="http://docs.oracle.com/javase/tutorial/java/javaOO/accesscontrol.html" class="alert-link">Controlling Access</a></strong> (1 page) in the Java Tutorials.</p>
</div>
-->
<p>We have been using <code>public</code> for almost all of our methods, without really thinking about it. The decision to make a method public or private is actually a decision about the contract of the class. Public methods are freely accessible to other parts of the program. Making a method public advertises it as a service that your class is willing to provide. If you make all your methods public — including helper methods that are really meant only for local use within the class — then other parts of the program may come to depend on them, which will make it harder for you to change the internal implementation of the class in the future. Your code won't be as <strong>ready for change</strong>. </p>
<p>Making internal helper methods public will also add clutter to the visible interface your class offers. Keeping internal things <code>private</code> makes your class's public interface smaller and more coherent (meaning that it does one thing and does it well). Your code will be <strong>easier to understand</strong>.</p>
<p>We will see even stronger reasons to use <code>private</code> in the next few classes, when we start to write classes with persistent internal state. Protecting this state will help keep the program <strong>safe from bugs</strong>.</p>
</div>
<h2 id="about_static_vs_instance_methods">About static vs. instance methods</h2>
<div data-outline="about_static_vs_instance_methods">
<!--
<div class="handout-solo alert alert-warning">
<p>Read: <strong><a href="http://www.codeguru.com/java/tij/tij0037.shtml#Heading79" class="alert-link">the <code>static</code> keyword</a></strong> on CodeGuru.</p>
</div>
-->
<p>We have also been using <code>static</code> for almost all of our methods, again without much discussion. Static methods are not associated with any particular instance of a class, while <code>instance</code> methods (declared without the <code>static</code> keyword) must be called on a particular object.</p>
<p>Specifications for instance methods are written just the same way as specifications for static methods, but they will often refer to properties of the instance on which they were called.</p>
<p>For example, by now we're very familiar with this specification:</p><pre class="no-markdown">static int find(int[] arr, int val)
<em>requires</em>: val occurs in arr
<em>effects</em>: returns index i such that arr[i] = val
</pre>
<p>Instead of using an <code>int[]</code>, what if we had a class <code>IntArray</code> designed for storing arrays of integers? The <code>IntArray</code> class might provide an instance method with the specification:</p><pre class="no-markdown">int find(int val)
<em>requires</em>: val occurs in *this array*
<em>effects</em>: returns index i such that *the value at index i in this array*
is val
</pre>
<p>We'll have much more to say about specifications for instance methods in future readings!</p>
</div>
</div>
</div>
</div>
</div>
<div class="xblock xblock-public_view xblock-public_view-vertical" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@vertical+block@vertical_Questions_cee5c5b9cfe2" data-block-type="vertical" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">Questions</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_fff67ba8819a">
<div class="xblock xblock-public_view xblock-public_view-html xmodule_display xmodule_HtmlBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_fff67ba8819a" data-block-type="html" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "HTMLModule"}
</script>
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<script src="/assets/courseware/v1/3e6443fb95285d2dc06e8ffc448b9bdf/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism.js"></script>
<script src="/assets/courseware/v1/2ba76f8bdfef4e2d45e31a3dc5208470/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/edx-script-v1.js"></script>
</div>
</div>
<div class="vert vert-1" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-show-me-a-sign">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-show-me-a-sign" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-show-me-a-sign" class="problems-wrapper" role="group"
aria-labelledby="05-show-me-a-sign-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-show-me-a-sign" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-show-me-a-sign/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-show-me-a-sign-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-show-me-a-sign-problem-progress" tabindex="-1">
show me a sign
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-show-me-a-sign-problem-progress"></div>
<div class="problem">
<div>
<p>Which of the following are signs of an excellent specification (check all that apply):</p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-show-me-a-sign_2_1">
<fieldset aria-describedby="status_05-show-me-a-sign_2_1">
<div class="field">
<input type="checkbox" name="input_05-show-me-a-sign_2_1[]" id="input_05-show-me-a-sign_2_1_choice_0" class="field-input input-checkbox" value="choice_0"/><label id="05-show-me-a-sign_2_1-choice_0-label" for="input_05-show-me-a-sign_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-show-me-a-sign_2_1"> 1. the specification is declarative
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-show-me-a-sign_2_1[]" id="input_05-show-me-a-sign_2_1_choice_1" class="field-input input-checkbox" value="choice_1"/><label id="05-show-me-a-sign_2_1-choice_1-label" for="input_05-show-me-a-sign_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-show-me-a-sign_2_1"> 2. the specification is operational
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-show-me-a-sign_2_1[]" id="input_05-show-me-a-sign_2_1_choice_2" class="field-input input-checkbox" value="choice_2"/><label id="05-show-me-a-sign_2_1-choice_2-label" for="input_05-show-me-a-sign_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-show-me-a-sign_2_1"> 3. the specification is as super-strong as possible
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-show-me-a-sign_2_1[]" id="input_05-show-me-a-sign_2_1_choice_3" class="field-input input-checkbox" value="choice_3"/><label id="05-show-me-a-sign_2_1-choice_3-label" for="input_05-show-me-a-sign_2_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-show-me-a-sign_2_1"> 4. the specification is as super-weak as possible
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-show-me-a-sign_2_1[]" id="input_05-show-me-a-sign_2_1_choice_4" class="field-input input-checkbox" value="choice_4"/><label id="05-show-me-a-sign_2_1-choice_4-label" for="input_05-show-me-a-sign_2_1_choice_4" class="response-label field-label label-inline" aria-describedby="status_05-show-me-a-sign_2_1"> 5. the implementation is allowed to ignore invalid arguments
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-show-me-a-sign_2_1[]" id="input_05-show-me-a-sign_2_1_choice_5" class="field-input input-checkbox" value="choice_5"/><label id="05-show-me-a-sign_2_1-choice_5-label" for="input_05-show-me-a-sign_2_1_choice_5" class="response-label field-label label-inline" aria-describedby="status_05-show-me-a-sign_2_1"> 6. the implementation is allowed to use different algorithms depending on the arguments
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-show-me-a-sign_2_1[]" id="input_05-show-me-a-sign_2_1_choice_6" class="field-input input-checkbox" value="choice_6"/><label id="05-show-me-a-sign_2_1-choice_6-label" for="input_05-show-me-a-sign_2_1_choice_6" class="response-label field-label label-inline" aria-describedby="status_05-show-me-a-sign_2_1"> 7. the specification utilizes the reader's knowledge of the implementation
</label>
</div>
<span id="answer_05-show-me-a-sign_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-show-me-a-sign_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-show-me-a-sign_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="show me a sign" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-show-me-a-sign" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-show-me-a-sign">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-show-me-a-sign-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-show-me-a-sign-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-show-me-a-sign-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-2" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-thats-an-odd-way-of-looking-at-it">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-thats-an-odd-way-of-looking-at-it" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-thats-an-odd-way-of-looking-at-it" class="problems-wrapper" role="group"
aria-labelledby="05-thats-an-odd-way-of-looking-at-it-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-thats-an-odd-way-of-looking-at-it" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-thats-an-odd-way-of-looking-at-it/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-thats-an-odd-way-of-looking-at-it-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-thats-an-odd-way-of-looking-at-it-problem-progress" tabindex="-1">
that&#39;s an odd way of looking at it
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-thats-an-odd-way-of-looking-at-it-problem-progress"></div>
<div class="problem">
<div>
<pre class="code">
public static int secondToLastIndexOf(int[] arr, int val)
requires: val appears in arr an odd number of times
effects: returns the 2nd-largest i such that arr[i] == val
</pre>
<p>Which of the following are reasonable criticisms of this spec? Check all that apply.</p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-thats-an-odd-way-of-looking-at-it_2_1">
<fieldset aria-describedby="status_05-thats-an-odd-way-of-looking-at-it_2_1">
<div class="field">
<input type="checkbox" name="input_05-thats-an-odd-way-of-looking-at-it_2_1[]" id="input_05-thats-an-odd-way-of-looking-at-it_2_1_choice_0" class="field-input input-checkbox" value="choice_0"/><label id="05-thats-an-odd-way-of-looking-at-it_2_1-choice_0-label" for="input_05-thats-an-odd-way-of-looking-at-it_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-thats-an-odd-way-of-looking-at-it_2_1"> The spec is not well-defined, we cannot implement it
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-thats-an-odd-way-of-looking-at-it_2_1[]" id="input_05-thats-an-odd-way-of-looking-at-it_2_1_choice_1" class="field-input input-checkbox" value="choice_1"/><label id="05-thats-an-odd-way-of-looking-at-it_2_1-choice_1-label" for="input_05-thats-an-odd-way-of-looking-at-it_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-thats-an-odd-way-of-looking-at-it_2_1"> The spec is not coherent
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-thats-an-odd-way-of-looking-at-it_2_1[]" id="input_05-thats-an-odd-way-of-looking-at-it_2_1_choice_2" class="field-input input-checkbox" value="choice_2"/><label id="05-thats-an-odd-way-of-looking-at-it_2_1-choice_2-label" for="input_05-thats-an-odd-way-of-looking-at-it_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-thats-an-odd-way-of-looking-at-it_2_1"> The spec is not deterministic
</label>
</div>
<div class="field">
<input type="checkbox" name="input_05-thats-an-odd-way-of-looking-at-it_2_1[]" id="input_05-thats-an-odd-way-of-looking-at-it_2_1_choice_3" class="field-input input-checkbox" value="choice_3"/><label id="05-thats-an-odd-way-of-looking-at-it_2_1-choice_3-label" for="input_05-thats-an-odd-way-of-looking-at-it_2_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-thats-an-odd-way-of-looking-at-it_2_1"> The spec is not operational
</label>
</div>
<span id="answer_05-thats-an-odd-way-of-looking-at-it_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-thats-an-odd-way-of-looking-at-it_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-thats-an-odd-way-of-looking-at-it_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="that&#39;s an odd way of looking at it" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-thats-an-odd-way-of-looking-at-it" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-thats-an-odd-way-of-looking-at-it">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-thats-an-odd-way-of-looking-at-it-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-thats-an-odd-way-of-looking-at-it-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-thats-an-odd-way-of-looking-at-it-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-3" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-behavioral-oddities">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-behavioral-oddities" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-behavioral-oddities" class="problems-wrapper" role="group"
aria-labelledby="05-behavioral-oddities-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-behavioral-oddities" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-behavioral-oddities/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="4"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-behavioral-oddities-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-behavioral-oddities-problem-progress" tabindex="-1">
behavioral oddities
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-behavioral-oddities-problem-progress"></div>
<div class="problem">
<div>
<p>Consider the following test cases for <code>secondToLastIndexOf</code>:</p>
<p><code>[ 1, 3, 4 ], 3</code> returns <code>1</code></p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-behavioral-oddities_2_1">
<fieldset aria-describedby="status_05-behavioral-oddities_2_1">
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_2_1" id="input_05-behavioral-oddities_2_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-behavioral-oddities_2_1-choice_0-label" for="input_05-behavioral-oddities_2_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_2_1"> valid test case
</label>
</div>
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_2_1" id="input_05-behavioral-oddities_2_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-behavioral-oddities_2_1-choice_1-label" for="input_05-behavioral-oddities_2_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_2_1"> could be valid with a weaker precondition, same postcondition
</label>
</div>
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_2_1" id="input_05-behavioral-oddities_2_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-behavioral-oddities_2_1-choice_2-label" for="input_05-behavioral-oddities_2_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_2_1"> could be valid with a weaker precondition, stronger postcondition
</label>
</div>
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_2_1" id="input_05-behavioral-oddities_2_1_choice_3" class="field-input input-radio" value="choice_3"/><label id="05-behavioral-oddities_2_1-choice_3-label" for="input_05-behavioral-oddities_2_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_2_1"> could be valid with same precondition, weaker postcondition
</label>
</div>
<span id="answer_05-behavioral-oddities_2_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-behavioral-oddities_2_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-behavioral-oddities_solution_1"/>
</div><p><code>[ 1, 3, 3, 4 ], 3</code> returns <code>1</code></p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 2" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-behavioral-oddities_3_1">
<fieldset aria-describedby="status_05-behavioral-oddities_3_1">
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_3_1" id="input_05-behavioral-oddities_3_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-behavioral-oddities_3_1-choice_0-label" for="input_05-behavioral-oddities_3_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_3_1"> valid test case
</label>
</div>
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_3_1" id="input_05-behavioral-oddities_3_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-behavioral-oddities_3_1-choice_1-label" for="input_05-behavioral-oddities_3_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_3_1"> could be valid with a weaker precondition, same postcondition
</label>
</div>
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_3_1" id="input_05-behavioral-oddities_3_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-behavioral-oddities_3_1-choice_2-label" for="input_05-behavioral-oddities_3_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_3_1"> could be valid with a weaker precondition, stronger postcondition
</label>
</div>
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_3_1" id="input_05-behavioral-oddities_3_1_choice_3" class="field-input input-radio" value="choice_3"/><label id="05-behavioral-oddities_3_1-choice_3-label" for="input_05-behavioral-oddities_3_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_3_1"> could be valid with same precondition, stronger postcondition
</label>
</div>
<span id="answer_05-behavioral-oddities_3_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-behavioral-oddities_3_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-behavioral-oddities_solution_2"/>
</div><p><code>[ 1, 3, 3, 3, 4 ], 3</code> returns <code>2</code></p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 3" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-behavioral-oddities_4_1">
<fieldset aria-describedby="status_05-behavioral-oddities_4_1">
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_4_1" id="input_05-behavioral-oddities_4_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-behavioral-oddities_4_1-choice_0-label" for="input_05-behavioral-oddities_4_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_4_1"> valid test case
</label>
</div>
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_4_1" id="input_05-behavioral-oddities_4_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-behavioral-oddities_4_1-choice_1-label" for="input_05-behavioral-oddities_4_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_4_1"> could be valid with a weaker precondition, same postcondition
</label>
</div>
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_4_1" id="input_05-behavioral-oddities_4_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-behavioral-oddities_4_1-choice_2-label" for="input_05-behavioral-oddities_4_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_4_1"> could be valid with a weaker precondition, stronger postcondition
</label>
</div>
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_4_1" id="input_05-behavioral-oddities_4_1_choice_3" class="field-input input-radio" value="choice_3"/><label id="05-behavioral-oddities_4_1-choice_3-label" for="input_05-behavioral-oddities_4_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_4_1"> could be valid with same precondition, stronger postcondition
</label>
</div>
<span id="answer_05-behavioral-oddities_4_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-behavioral-oddities_4_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-behavioral-oddities_solution_3"/>
</div><p><code>[ 3, 3, 3, 3 ], 3</code> throws an exception</p>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 4" role="group"><div class="choicegroup capa_inputtype" id="inputtype_05-behavioral-oddities_5_1">
<fieldset aria-describedby="status_05-behavioral-oddities_5_1">
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_5_1" id="input_05-behavioral-oddities_5_1_choice_0" class="field-input input-radio" value="choice_0"/><label id="05-behavioral-oddities_5_1-choice_0-label" for="input_05-behavioral-oddities_5_1_choice_0" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_5_1"> valid test case
</label>
</div>
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_5_1" id="input_05-behavioral-oddities_5_1_choice_1" class="field-input input-radio" value="choice_1"/><label id="05-behavioral-oddities_5_1-choice_1-label" for="input_05-behavioral-oddities_5_1_choice_1" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_5_1"> could be valid with a weaker precondition, same postcondition
</label>
</div>
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_5_1" id="input_05-behavioral-oddities_5_1_choice_2" class="field-input input-radio" value="choice_2"/><label id="05-behavioral-oddities_5_1-choice_2-label" for="input_05-behavioral-oddities_5_1_choice_2" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_5_1"> could be valid with a weaker precondition, stronger postcondition
</label>
</div>
<div class="field">
<input type="radio" name="input_05-behavioral-oddities_5_1" id="input_05-behavioral-oddities_5_1_choice_3" class="field-input input-radio" value="choice_3"/><label id="05-behavioral-oddities_5_1-choice_3-label" for="input_05-behavioral-oddities_5_1_choice_3" class="response-label field-label label-inline" aria-describedby="status_05-behavioral-oddities_5_1"> could be valid with same precondition, stronger postcondition
</label>
</div>
<span id="answer_05-behavioral-oddities_5_1"/>
</fieldset>
<div class="indicator-container">
<span class="status unanswered" id="status_05-behavioral-oddities_5_1" data-tooltip="Not yet answered.">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-behavioral-oddities_solution_4"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="behavioral oddities" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-behavioral-oddities" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-behavioral-oddities">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-behavioral-oddities-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-behavioral-oddities-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-behavioral-oddities-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
<div class="vert vert-4" data-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-odd-doc">
<div class="xblock xblock-public_view xblock-public_view-problem xmodule_display xmodule_ProblemBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-odd-doc" data-block-type="problem" data-graded="True" data-has-score="True" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Problem"}
</script>
<div id="problem_05-odd-doc" class="problems-wrapper" role="group"
aria-labelledby="05-odd-doc-problem-title"
data-problem-id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-odd-doc" data-url="/courses/course-v1:MITx+6.005.1x+3T2016/xblock/block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-odd-doc/handler/xmodule_handler"
data-problem-score="0"
data-problem-total-possible="1"
data-attempts-used="0"
data-content="
<h3 class="hd hd-3 problem-header" id="05-odd-doc-problem-title" aria-describedby="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-odd-doc-problem-progress" tabindex="-1">
odd doc
</h3>
<div class="problem-progress" id="block-v1:MITx+6.005.1x+3T2016+type@problem+block@05-odd-doc-problem-progress"></div>
<div class="problem">
<div>
<p>Here's the spec again:</p>
<pre class="code">
public static int secondToLastIndexOf(int[] arr, int val)
requires: val appears in arr an odd number of times
effects: returns the 2nd-largest i such that arr[i] == val
</pre>
<div class="wrapper-problem-response" tabindex="-1" aria-label="Question 1" role="group"><div id="inputtype_05-odd-doc_2_1" class="choicegroup capa_inputtype">
<fieldset aria-describedby="status_05-odd-doc_2_1">
<legend id="05-odd-doc_2_1-legend" class="response-fieldset-legend field-group-hd">Choose lines below to complete one possible Javadoc version of this terrible spec:</legend>
<div class="field">
<input id="input_05-odd-doc_2_1_choice_0" type="checkbox" name="input_05-odd-doc_2_1[]" class="field-input input-checkbox" value="choice_0"/><label id="05-odd-doc_2_1-choice_0-label" for="input_05-odd-doc_2_1_choice_0" aria-describedby="status_05-odd-doc_2_1" class="response-label field-label label-inline"> /*
</label>
</div>
<div class="field">
<input id="input_05-odd-doc_2_1_choice_1" type="checkbox" name="input_05-odd-doc_2_1[]" class="field-input input-checkbox" value="choice_1"/><label id="05-odd-doc_2_1-choice_1-label" for="input_05-odd-doc_2_1_choice_1" aria-describedby="status_05-odd-doc_2_1" class="response-label field-label label-inline"> /**
</label>
</div>
<div class="field">
<input id="input_05-odd-doc_2_1_choice_2" type="checkbox" name="input_05-odd-doc_2_1[]" class="field-input input-checkbox" value="choice_2"/><label id="05-odd-doc_2_1-choice_2-label" for="input_05-odd-doc_2_1_choice_2" aria-describedby="status_05-odd-doc_2_1" class="response-label field-label label-inline"> * Finds the second-to-last occurence of a value in an array.
</label>
</div>
<div class="field">
<input id="input_05-odd-doc_2_1_choice_3" type="checkbox" name="input_05-odd-doc_2_1[]" class="field-input input-checkbox" value="choice_3"/><label id="05-odd-doc_2_1-choice_3-label" for="input_05-odd-doc_2_1_choice_3" aria-describedby="status_05-odd-doc_2_1" class="response-label field-label label-inline"> * Find j, the largest index such that arr[j] == val.
</label>
</div>
<div class="field">
<input id="input_05-odd-doc_2_1_choice_4" type="checkbox" name="input_05-odd-doc_2_1[]" class="field-input input-checkbox" value="choice_4"/><label id="05-odd-doc_2_1-choice_4-label" for="input_05-odd-doc_2_1_choice_4" aria-describedby="status_05-odd-doc_2_1" class="response-label field-label label-inline"> * Then find i, the largest index such that i &lt; j and arr[i] == val.
</label>
</div>
<div class="field">
<input id="input_05-odd-doc_2_1_choice_5" type="checkbox" name="input_05-odd-doc_2_1[]" class="field-input input-checkbox" value="choice_5"/><label id="05-odd-doc_2_1-choice_5-label" for="input_05-odd-doc_2_1_choice_5" aria-describedby="status_05-odd-doc_2_1" class="response-label field-label label-inline"> * @param arr array to search
</label>
</div>
<div class="field">
<input id="input_05-odd-doc_2_1_choice_6" type="checkbox" name="input_05-odd-doc_2_1[]" class="field-input input-checkbox" value="choice_6"/><label id="05-odd-doc_2_1-choice_6-label" for="input_05-odd-doc_2_1_choice_6" aria-describedby="status_05-odd-doc_2_1" class="response-label field-label label-inline"> * @param arr fixed-size array of integers to search
</label>
</div>
<div class="field">
<input id="input_05-odd-doc_2_1_choice_7" type="checkbox" name="input_05-odd-doc_2_1[]" class="field-input input-checkbox" value="choice_7"/><label id="05-odd-doc_2_1-choice_7-label" for="input_05-odd-doc_2_1_choice_7" aria-describedby="status_05-odd-doc_2_1" class="response-label field-label label-inline"> * @param val value to search for
</label>
</div>
<div class="field">
<input id="input_05-odd-doc_2_1_choice_8" type="checkbox" name="input_05-odd-doc_2_1[]" class="field-input input-checkbox" value="choice_8"/><label id="05-odd-doc_2_1-choice_8-label" for="input_05-odd-doc_2_1_choice_8" aria-describedby="status_05-odd-doc_2_1" class="response-label field-label label-inline"> * @param val value to search for, requires val appears in arr an odd number of times
</label>
</div>
<div class="field">
<input id="input_05-odd-doc_2_1_choice_9" type="checkbox" name="input_05-odd-doc_2_1[]" class="field-input input-checkbox" value="choice_9"/><label id="05-odd-doc_2_1-choice_9-label" for="input_05-odd-doc_2_1_choice_9" aria-describedby="status_05-odd-doc_2_1" class="response-label field-label label-inline"> * @return index i
</label>
</div>
<div class="field">
<input id="input_05-odd-doc_2_1_choice_10" type="checkbox" name="input_05-odd-doc_2_1[]" class="field-input input-checkbox" value="choice_10"/><label id="05-odd-doc_2_1-choice_10-label" for="input_05-odd-doc_2_1_choice_10" aria-describedby="status_05-odd-doc_2_1" class="response-label field-label label-inline"> * @return second-largest index i such that arr[i] == val
</label>
</div>
<div class="field">
<input id="input_05-odd-doc_2_1_choice_11" type="checkbox" name="input_05-odd-doc_2_1[]" class="field-input input-checkbox" value="choice_11"/><label id="05-odd-doc_2_1-choice_11-label" for="input_05-odd-doc_2_1_choice_11" aria-describedby="status_05-odd-doc_2_1" class="response-label field-label label-inline"> */
</label>
</div>
<span id="answer_05-odd-doc_2_1"/>
</fieldset>
<div class="indicator-container">
<span id="status_05-odd-doc_2_1" data-tooltip="Not yet answered." class="status unanswered">
<span class="sr">unanswered</span><span class="status-icon" aria-hidden="true"/>
</span>
</div>
</div></div>
<div class="solution-span">
<span id="solution_05-odd-doc_solution_1"/>
</div></div>
<div class="action">
<input type="hidden" name="problem_id" value="odd doc" />
<div class="submit-attempt-container">
<button type="button" class="submit btn-brand" data-submitting="Submitting" data-value="Submit" data-should-enable-submit-button="True" aria-describedby="submission_feedback_05-odd-doc" >
<span class="submit-label">Submit</span>
</button>
<div class="submission-feedback" id="submission_feedback_05-odd-doc">
<span class="sr">Some problems have options such as save, reset, hints, or show answer. These options follow the Submit button.</span>
</div>
</div>
<div class="problem-action-buttons-wrapper">
</div>
</div>
<div class="notification warning notification-gentle-alert
is-hidden"
tabindex="-1">
<span class="icon fa fa-exclamation-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-odd-doc-problem-title">
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification warning notification-save
is-hidden"
tabindex="-1">
<span class="icon fa fa-save" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-odd-doc-problem-title">None
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
<div class="notification general notification-show-answer
is-hidden"
tabindex="-1">
<span class="icon fa fa-info-circle" aria-hidden="true"></span>
<span class="notification-message" aria-describedby="05-odd-doc-problem-title">Answers are displayed within the problem
</span>
<div class="notification-btn-wrapper">
<button type="button" class="btn btn-default btn-small notification-btn review-btn sr">Review</button>
</div>
</div>
</div>
"
data-graded="True">
<p class="loading-spinner">
<i class="fa fa-spinner fa-pulse fa-2x fa-fw"></i>
<span class="sr">Loading…</span>
</p>
</div>
</div>
</div>
</div>
</div>
<div class="xblock xblock-public_view xblock-public_view-vertical" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@vertical+block@Reading_5_Summary" data-block-type="vertical" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">Reading 5 Summary</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_f15dff657c02">
<div class="xblock xblock-public_view xblock-public_view-html xmodule_display xmodule_HtmlBlock" data-runtime-version="1" data-usage-id="block-v1:MITx+6.005.1x+3T2016+type@html+block@html_f15dff657c02" data-block-type="html" data-graded="True" data-has-score="False" data-course-id="course-v1:MITx+6.005.1x+3T2016" data-runtime-class="LmsRuntime" data-request-token="2935fb7a4c3911ef89500e6e8f39bb05" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "HTMLModule"}
</script>
<link href="/assets/courseware/v1/9fab367942e94f98d32835b3ef4df11d/asset-v1:MITx+6.005.1x+3T2016+type@asset+block/prism-edx-v1.css" rel="stylesheet" type="text/css" />
<h2>Summary</h2>
<p>A specification acts as a crucial firewall between implementor and client — both between people (or the same person at different times) and between code. As we saw in the previous reading, it makes separate development possible: the client is free to write code that uses a module without seeing its source code, and the implementor is free to write the implementation code without knowing how it will be used.</p>
<p>Declarative specifications are the most useful in practice. Preconditions (which weaken the specification) make life harder for the client, but applied judiciously they are a vital tool in the software designer's repertoire, allowing the implementor to make necessary assumptions.</p>
<p>As always, our goal is to design specifications that make our software:</p>
<ul>
<li>
<p><strong>Safe from bugs.</strong> Without specifications, even the tiniest change to any part of our program could be the tipped domino that knocks the whole thing over. Well-structured, coherent specifications minimize misunderstandings and maximize our ability to write correct code with the help of static checking, careful reasoning, testing, and code review.</p>
</li>
<li>
<p><strong>Easy to understand.</strong> A well-written declarative specification means the client doesn't have to read or understand the code. You've probably never read the code for, say, <a href="https://hg.python.org/cpython/file/7ae156f07a90/Objects/dictobject.c#l1990">Python dict.update</a>, and doing so isn't nearly as useful to the Python programmer as <a href="https://docs.python.org/3/library/stdtypes.html#dict.update">reading the declarative spec</a>.</p>
</li>
<li>
<p><strong>Ready for change.</strong> An appropriately weak specification gives freedom to the implementor, and an appropriately strong specification gives freedom to the client. We can even change the specs themselves, without having to revisit every place they're used, as long as we're only strengthening them: weakening preconditions and strengthening postconditions.</p>
</li>
</ul>
<div class="license">This reading was collaboratively authored with contributions from: Saman Amarasinghe, Adam Chlipala, Srini Devadas, Michael Ernst, Max Goldman, John Guttag, Daniel Jackson, Rob Miller, Martin Rinard, and Armando Solar-Lezama. This work is licensed under <a rel="license" href="http://creativecommons.org/licenses/by-sa/4.0/">CC BY-SA 4.0</a>.</div>
</div>
</div>
</div>
</div>