[an error occurred while processing this directive]
<meta NAME="ROBOTS" CONTENT="index,follow">
<meta NAME="keywords" CONTENT=" contract, assertion, development, course, attending, oriented, programming, semantics, basic, capabilities, object, knowledge, imperative, invariants, learn, understand, checking, approach, writing, design, correctness, students, techniques, state, tools, postconditions, preconditions, programs, code, hoare, help, example, runtime, testing, logic, static, foundational, undecidability, documentation, particular, introduced, objectives, introduction, requirements, propositional, advantages, abstraction, reasoning, operational, behaviour, approaches, challenges, debugging, recommended, generating, refinement, employed, separation, formally, strongest, practicals, explosion, thinking, identify, concepts, analysis, extending, contents, defined, planned, exercises, broader, smaller, improve, language, weakest, familiar, teaching, during, stages, prestudy, meaning, partial, better, complex, working, ideally, pieces, reason, useful, solving, further, common, phase, later, giving, formal, works, simple, dates">
<meta name="DESCRIPTION" content="Robust Programming course This course will present foundational techniques for reasoning about the behaviour of object oriented and imperative programs Students will learn how these techniques can be employed during the design phase or at later stages of development In particular, they will see how semantics can be formally defined and how static checking works, and will be introduced to the design by contract approach ">


<meta name="Edited" content="Mon, 31 Dec 2018 19:20:03 GMT">
<meta name="Published" content="Mon, 31 Dec 2018 19:20:13 GMT">

<title>Software Engineering at Oxford | Robust Programming ( ROP )</title>

<!-- icon -->
<link rel="shortcut icon" type="image/ico" href="../favicon.ico">

<script src="https://ssl.google-analytics.com/urchin.js" type="text/javascript"></script>
<script type="text/javascript">_uacct = "UA-1306673-1";urchinTracker();/*UA-579489-1*/</script>
<META name="verify-v1" content="CwYQSB0rDIbG5v7tQy+2xKxvNEoOxCNSFYYF7mSW7bo=" />
[an error occurred while processing this directive]

<div id="breadcrumb">
   
   <ul class="mainnav">
      <li>
         <a href="/">Computer Science</a></li><li><a href="/softeng/">Software Engineering</a>
      </li>
      <li>
         <a href="/softeng/courses/">Courses</a>
      </li>
      <li>
         <a href="/softeng/courses/subjects.html">Subjects</a>
      </li>
      <li>
         <span class="youarehere">Robust Programming ( ROP )</span>
      </li>
   </ul>
</div>


<!--
<span id="headerItem">
  <a href="../programme/contact.html" title="Contacts">Contact</a> | 
  <a href="../search/search.jsp" title="Search">Search</a> |
  <a href="../sitemap.html" title="Sitemap">Site map</a> | 
  <a href="https://www.softeng.ox.ac.uk/signin/" title="Sign in">Sign
  in</a>
</span>
-->

<div id="content">

<table cellpadding="0" cellspacing="0" border="0"><tr><td style="width: 75px"><div style="width: 75px;height: 75px"><div style="width: 55px;height: 55px; margin: 10px;-moz-box-shadow: 0px 5px 5px rgba(0,0,0,0.3), -2px 1px 5px rgba(0,0,0,0.3), 2px 1px 5px rgba(0,0,0,0.3); -webkit-box-shadow: 0px 5px 5px rgba(0,0,0,0.3), -2px 1px 5px rgba(0,0,0,0.3), 2px 1px 5px rgba(0,0,0,0.3); box-shadow: 0px 5px 5px rgba(0,0,0,0.3), -2px 1px 5px rgba(0,0,0,0.3), 2px 1px 5px rgba(0,0,0,0.3);-moz-border-radius: 8px;-webkit-border-radius: 8px; border-radius: 8px;" id="ROPBg"><div style="font-size: 14px; font-weight: bold; text-align:center; position: relative; top: 20px; background-color: transparent; color: white">ROP</div></div></div></td><td style="vertical-align:middle"><h1>Robust Programming</h1></td></tr></table>
      <div>
	
	<p>This course will present foundational techniques for reasoning about the behaviour of object-oriented and imperative programs. Students will learn how these techniques can be employed during the design phase or at later stages of development. In particular, they will see how semantics can be formally defined and how static checking works, and will be introduced to the design-by-contract approach.</p>
<h4>Course dates</h4>
<center>
Future courses yet to be planned.<br>
</center>
<h4>Objectives</h4>
<p><p>After attending the course, the students will understand:</p>
<ul>
<li>ways of thinking about semantics of programs;</li>
<li>how assertions can help debugging and writing better code;</li>
<li>how to identify loop invariants;</li>
<li>how to &ldquo;prove&rdquo; correctness of programs using Hoare logic;</li>
<li>basic concepts and advantages of the design-by-contract approach;</li>
<li>capabilities of state-of-the-art static analysis tools.  In broader terms, this knowledge will help students understand how to break programming tasks into smaller pieces and reason about them, or how to improve their code testing.</li>
</ul></p>
<h4>Contents</h4>
<p><ul>
<li>Runtime assertion checking: pros and cons of runtime checking and testing.</li>
<li>Writing useful assertions: preconditions and postconditions, invariants, weakest preconditions and strongest postconditions.</li>
<li>Static checking: common approaches and main challenges (undecidability, state-space explosion), tools and their capabilities.</li>
<li>Design by contract: use for development, testing, generating documentation and for static checking; abstraction and refinement of contracts.</li>
<li>Operational semantics: giving formal meaning to imperative programs.</li>
<li>Hoare logic for simple imperative programs: partial correctness, total correctness. Extending Hoare logic to more complex data types: brief introduction to separation logic.</li>
</ul></p>
<h4>Requirements</h4>
<p>The students should have a working knowledge of an object oriented programming language (ideally C# or Java). The practicals will be mainly done in C#, and hence it is recommended that students not familiar with it learn its basic syntax before the teaching week, for example by solving exercises given as part of the prestudy.

Further, students should know the basics of set theory and propositional logic, for example gained by attending SEM.</p>

	
      </div>

<br>

    
[an error occurred while processing this directive]

<!--  mainnav div starts -->
<div id="nav">     
 <h2 id="mainsections">Main sections</h2>
 
 <h2 id="inthissection">Programme</h2>
 <ul class="mainnav" >
  <li>
   <a href="../" title="Return to the Home page" class="menu" >Home</a>
  </li>
  <li>
   <a href="../programme/index.html" title="About the programme" class="menu">About</a>
  </li>
  <li>
   <a href="../programme/history.html" title="The history of the Programme"  class="menu">History</a>
  </li>
  <li>
   <a href="../programme/people.html" title="The people involved" class="menu">People</a>
  </li>
  <li>
   <a href="http://www.cs.ox.ac.uk" title="Department of Computer Science" class="menu">Department</a>
  </li>
  <li>
   <a href="../programme/contact.html" title="Getting in touch" class="menu">Contact us</a>
  </li>
  </ul>
  
  
  <h2 id="inthissection">Courses</h2>
  <ul class="mainnav">
  <li>
   <a href="../courses/" title="About the courses" class="menu">About</a>
  </li>
  <li>
   <a href="../courses/subjects.html" title="Subjects offered" class="currentsection">Subjects</a>
  </li>
  <li>
   <a href="../courses/calendar.html" title="Course dates" class="menu">Calendar</a>
  </li>
  <li>
   <a href="../courses/booking.html" title="How to book a place on a course" class="menu">Booking</a>
  </li>
  </ul>
  
  
  <h2 id="inthissection">Study</h2>
  <ul class="mainnav">
  <li>
   <a href="../study/" title="Flexible, postgraduate study" class="menu">About</a>
  </li>
  <li>
   <a href="../study/awards.html" title="Academic awards" class="menu">Awards</a>
  </li>
  <li>
   <a href="../study/fees.html" title="University fees" class="menu">Fees</a>
  </li>
  <li>
   <a href="../study/apply.html" title="How to apply" class="menu">Applications</a>
  </li>
  <li>
   <a href="../study/collegiate.html" title="Collegiate University" class="menu">Colleges</a>
  </li>
  </ul>
  
  
  <h2 id="inthissection">Resources</h2>
  <ul class="mainnav">
  <li>
   <a href="../handbook/" title="Handbook" class="menu">Handbook</a>
  </li>
  <li>
   <a href="../brochures/" title="Brochures" class="menu">Brochures</a>
  </li>
 </ul>



[an error occurred while processing this directive]