<?xml version="1.0" encoding="utf-8"?><!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Publishing DTD v1.0 20120330//EN" "JATS-journalpublishing1.dtd"><article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink" article-type="article">
<front>
    <journal-meta>
        <journal-id journal-id-type="publisher-id">INFEDU</journal-id>
        <journal-title-group>
            <journal-title>Informatics in Education</journal-title>
        </journal-title-group>
        <issn pub-type="epub">1648-5831</issn>
        <issn pub-type="ppub">1648-5831</issn>
        <publisher>
            <publisher-name>VU</publisher-name>
        </publisher>
    </journal-meta>
    <article-meta>
                <article-id pub-id-type="publisher-id">INFE163</article-id>
                        <article-id pub-id-type="doi">10.15388/infedu.2010.07</article-id>
                        <article-categories>
            <subj-group subj-group-type="heading">
                <subject>Article</subject>
            </subj-group>
        </article-categories>
                        <title-group>
            <article-title>Invariant Based Programming in Education - An Analysis of Student Difficulties</article-title>
        </title-group>
                        <contrib-group>
                                        <contrib contrib-type="author">
                                                <name>
                    <surname>MANNILA</surname>
                    <given-names>Linda</given-names>
                </name>
                                <email xlink:href="mailto:linda.mannila@abo.fi">linda.mannila@abo.fi</email>
                                                <xref ref-type="aff" rid="j_INFEDU_aff_000"/>
                                            </contrib>
                        <aff id="j_INFEDU_aff_000">Department of Information Technologies, Åbo Akademi University Turku Centre for Computer Science Joukahaisenkatu 3-5 A, 20520 Turku, Finland</aff>
                                </contrib-group>
                                                                            <volume>9</volume>
                                <issue>1</issue>
                                    <fpage>115</fpage>
                        <lpage>132</lpage>
						<pub-date pub-type="epub">
                        <day>15</day>
                                    <month>04</month>
                        <year>2010</year>
        </pub-date>
                                                        <abstract>
                        <p>In this paper, we analyze the errors novice students make when developing invariant based programs. In addition to presenting the general error types, we also look at what students have difficulty with when it comes to expressing invariants. The results indicate that an introductory course utilizing the invariant based approach is suitable from the very beginning of university studies in CS without being ``too advanced&#039;&#039;. Although inventing the invariant was not found to be trivial, the main difficulty faced by novices when applying a correct-by-construction approach to program development seems to be related to weak skills in translating intuitive and informal statements into a symbolic form using logical notation in general and quantifiers in particular.</p>
                    </abstract>
                <kwd-group>
            <label>Keywords</label>
                        <kwd>invariant based programming</kwd>
                        <kwd>programming education</kwd>
                        <kwd>introductory formal methods</kwd>
                        <kwd>student difficulties</kwd>
                    </kwd-group>
    </article-meta>
</front>
</article>
