欢迎来到麦多课文档分享! | 帮助中心 海量文档,免费浏览,给你所需,享你所想!
麦多课文档分享
全部分类
  • 标准规范>
  • 教学课件>
  • 考试资料>
  • 办公文档>
  • 学术论文>
  • 行业资料>
  • 易语言源码>
  • ImageVerifierCode 换一换
    首页 麦多课文档分享 > 资源分类 > PPT文档下载
    分享到微信 分享到微博 分享到QQ空间

    Engaging Students in Specification and Reasoning- Hands-.ppt

    • 资源ID:374430       资源大小:230KB        全文页数:21页
    • 资源格式: PPT        下载积分:2000积分
    快捷下载 游客一键下载
    账号登录下载
    微信登录下载
    二维码
    微信扫一扫登录
    下载资源需要2000积分(如需开发票,请勿充值!)
    邮箱/手机:
    温馨提示:
    如需开发票,请勿充值!快捷下载时,用户名和密码都是您填写的邮箱或者手机号,方便查询和重复下载(系统自动生成)。
    如需开发票,请勿充值!如填写123,账号就是123,密码也是123。
    支付方式: 支付宝扫码支付    微信扫码支付   
    验证码:   换一换

    加入VIP,交流精品资源
     
    账号:
    密码:
    验证码:   换一换
      忘记密码?
        
    友情提示
    2、PDF文件下载后,可能会被浏览器默认打开,此种情况可以点击浏览器菜单,保存网页到桌面,就可以正常下载了。
    3、本站不支持迅雷下载,请使用电脑自带的IE浏览器,或者360浏览器、谷歌浏览器下载即可。
    4、本站资源下载后的文档和图纸-无水印,预览文档经过压缩,下载后原文更清晰。
    5、试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓。

    Engaging Students in Specification and Reasoning- Hands-.ppt

    1、Engaging Students in Specification and Reasoning: Hands-On Experimentation and Evaluation,Murali Sitaraman, Jason Hallstrom, Jarred White, Svetlana Drachova-Strang, Heather Harton, Dana Leonard: Clemson University School of Computing. Joan Krone : Denison University. Rich Pak: Clemson University Psy

    2、chology.Supported by US NSF #3407328,2,Goal,Reasoning Across the Curriculum Supporting Tools Supporting Methods,3,4,Software Engineering Course,Usual Topics Requirements analysis Design and specification Component-based implementation Quality assurance Formal Reasoning,5,Objectives,Read formal speci

    3、fications Create test points from the specs Use component specifications to build larger systems Work in teams Carry out formal verification of components Use automated rules,6,Methods,Collaborative learning Teams of 2 to 4 members Read specs Implement specs Verify implementations Build larger syste

    4、ms.,7,Stack Example,Model as a mathematical string of generic entries with an upper limit of Max_Depth. Initialize as empty string. Oper Push(eval E: Entry; updates S: Stack);requires |S| Max_Depth;ensures S = E o #S;,8,Reading Specs,Give students various strings representing abstract stacks and tel

    5、l what Max_Depth is. Ask them to show what happens when a Push is called with particular data. Ex: S = rtb Max_Depth = 5. Push(c,S) Push(w,S),9,Queue Example,Model as a string of generic entries. Primary operations: enqueue, dequeue, length. Secondary operation,10,Test Cases for Rotate,Oper Rotate(u

    6、pdates Q: Queue, restores n: Integer); requires |Q| n = 3; Output: Q = n = 3; #Q = Input Q, Q = output Q S = T = ,11,Tools,Specification Understanding: Expose students to formal specifications for reasoning. Team Software Development with Formal Contract Specifications: Enforce contract programming

    7、principles. Verification Condition Generation: Generate clauses equivalent to the correctness of the implementation.,Using the Tools,http:/www.cs.clemson.edu/resolve,12,13,Survey Questions,(S3) The difficulty in understanding and modifying a 10,000 line software system has more to do with the style

    8、I which the software is written, and less to do with how smart I am. (S11) Testing software thoroughly is the most important way to ensure correctness.,14,Results for S11,15,(S18) When working in teams, natural language descriptions of the different components are sufficient for communication among

    9、team members. (S20) Reasoning about programs involving components requires a thorough understanding of pointers and/or references. Entire survey at http:/www.cs.clemson.edu/resolve,16,Results for S18,All Results,http:/www.cs.clemson.edu/resolve/,17,RSRG: Tools for Teaching Mathematical Specification

    10、 and ReasoningWe are currently documenting tools and results for integrating mathematical specification and reasoning in undergraduate classes with support from an NSF CCLI grant. For an overview as well as how we have introduced the methods and tools in a software engineering course, please see thi

    11、s technical report: M. Sitaraman, J. O. Hallstrom, J. White, S. Drachova-Strang, H. K. Harton, D. Leonard, J. Krone, and R. Pak, Engaging Students in Specification and Reasoning: “Hands-On” Experimentation and Evaluation, Technical Report RSRG-08-05, School of Computing, Clemson University, Clemson,

    12、 SC 29634-0974, December 2008, 6 pages. For materials on how the principles have been introduced in a sophomore level course on object-oriented development with Java, please visit CP SC 215 course links under teaching at these sites: Fall 2008: http:/www.cs.clemson.edu/murali Spring 2009: http:/www.

    13、cs.clemson.edu/jasonoh,Specification Understanding: One of the software engineering objectives of all undergraduate curricula in computing is to at least expose students to formal specifications of behavior. These specifications are presented formally in mathematical logic and can be written in a va

    14、riety of formal specification languages. For an overview and to download the tool, click here. Details of the tool are discussed in the following paper:D. Leonard, J. Hallstrom, and M. Sitaraman, “Injecting Rapid Feedback and Collaborative Reasoning in Teaching Specifications,” ACM SIGCSE 2009 Procs

    15、. at http:/db.grinnell.edu/sigcse/sigcse2009/Program/Program.asp Team Software Development with Formal Contract Specifications: RESOLVE analyzer and RESOLVE-to-Java translator is available here to enable formal contract-based software development. For a technical summary of how we have introduced th

    16、e ideas in a software engineering course, please see this technical report: S. Drachavo-Strang, Teaching Design-By-Contract with Formal Specifications, which is available here. Verification Condition Generation: For an overview of methods and tools to teach proofs of correctness and formal mathemati

    17、cal reasoning about correctness of programs, please see here. For technical details on a push-button verification system, please see this technical report: M. Sitaraman, B. Adcock, J. Avigad, D. Bronish, P. Bucci, D. Frazier, H. M. Friedman, H. Harton, W. Heym, J. Kirschenbaum, J. Krone, H. Smith, a

    18、nd B. W. Weide, Building a Push-Button RESOLVE Verifier: Progress and Challenges, Technical Report RSRG-09-01, School of Computing, Clemson University, Clemson, SC 29634-0974, January 2009, 34 pages.,Demos,http:/resolve.cs.clemson.edu/,20,Summary,Importance of Reasoning across the Curriculum Tools to Support Reasoning Collaborative Pedagogy includes collaboration between students and between students and faculty,21,


    注意事项

    本文(Engaging Students in Specification and Reasoning- Hands-.ppt)为本站会员(sofeeling205)主动上传,麦多课文档分享仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对上载内容本身不做任何修改或编辑。 若此文所含内容侵犯了您的版权或隐私,请立即通知麦多课文档分享(点击联系客服),我们立即给予删除!




    关于我们 - 网站声明 - 网站地图 - 资源地图 - 友情链接 - 网站客服 - 联系我们

    copyright@ 2008-2019 麦多课文库(www.mydoc123.com)网站版权所有
    备案/许可证编号:苏ICP备17064731号-1 

    收起
    展开