• 赵孟頫:书法大师是怎么炼成的? 2019-06-17
  • 工业互联网支持政策密集出台 2019-06-09
  • 强势发力体育营销 世界杯中国企业改变“旁观”窘状 2019-06-09
  • 小型地铺: 规模较小,中介费较实惠 2019-06-09
  • 以色列:卷入贪腐案  以总理接受警方调查 2019-06-09
  • 亳州留置“第一案”审理!谯城区一书记被指控 2019-06-08
  • 一周人事:国务院发布任免刘伟当选北京市总工会主席 2019-06-07
  • 【十九大·理论新视野】动漫:“社会主义现代化强国”如何建成 2019-06-07
  • 第530期:为何吃新鲜蔬果能抗肿瘤、强免疫……?因为有“它”! 2019-06-06
  • 贵州遵义:完善本土专技人才培养工程 2019-06-06
  • 太美了!合肥初雪航拍 看完想在雪地打滚 2019-06-05
  • 浙江省网络文明公益宣传创意作品展示 2019-06-05
  • 沈阳国际徒步日活动将于16日举行 超3万人参与 2019-06-04
  • 食品舆情:京东回应“假茅台”系被调包 饿了么推出可食用筷子宣传环保 2019-06-03
  • 青岛峰会为世界注入强大正能量(钟声) 2019-06-02
  • 当前位置:香港赛马会928282_com > Declarative View of Imperative Programs Hugh

    Declarative View of Imperative Programs Hugh

    香港赛马会928282_com www.jonqp.tw Declarative View of Imperative Programs

    Hugh Gibbons,

    Trinity College,

    Dublin,

    Ireland.

    Abstract

    By giving a declarative meaning to an imperative program, the verification of the imperative program is

    switched from the imperative paradigm to the declarative or logic paradigm where one can take advantage

    of, for example, referential transparency. Rather than ‘compiling’ an imperative program to a ‘lower level’

    we ‘inverse compile’ the imperative program to the ‘higher’ declarative level. The declarative view of an

    imperative program is a predicate associated with the imperative program such that if this predicate satisfies

    the specification of the program then the imperative program is correct relative to the specification. In one

    sense the associated predicate gives a declarative meaning to the imperative program.

    “… and I do consider assignment statements and pointer variables to be among computer science’s ‘most valuable treasures’.”

    D. Knuth [5]

    1.Introduction

    In imperative programming, programs are implicitly state transformations. We want to abstract away from dealing with states and try to express programs within the “problem domain”, that is, we want to give a declarative meaning to imperative programs. If we want to sort a list, our program for doing this should deal with lists and use the properties of lists. Logic/Functional programming and also programming with assertions allow us to do this abstraction. Imperative programs may have functional and relational features - functions and procedures - but they also contain constructs which deal only with state transformation e.g. the assignment statement.

    “Not only goto statements are being questioned: we hear complaints about floating-point calculations, global variables, semaphores, pointer variables, and even assignment statements.”

    D. Knuth [6]

    We are assuming a structured programming language without “goto” and the aim is to transform a structured program to a program without an assignment. We are not just complaining about the ‘assignment statement’, our aim is to show how it can be removed from programming. Without the assignment statement we gain the advantage of referential transparency (‘substitution of equals for equals’) which allows both for easier program verification and easier program construction. Also, by transforming a structured program to an ‘assignment-less’program we indicate a non-operational declarative meaning to the program.

    2.Associating a Predicate with an Imperative Program.

    In the axiomatic semantics of Hoare/Dijkstra/Gries, a predicat
    e pair gives the meaning of the imperative program and in this context a program is viewed as a predicate transformer, transforming a predicate to a predicate. For example, if we have a program, MOD, that calculates the ‘integer modulo function’ then the predicate pair

    In the axiomatic semantics of Hoare/Dijkstra/Gries, a predicate pair gives the meaning of the imperative program and in this context a program is viewed as a predicate transformer, transforming a predicate to a predicate. For example, if we have a program, MOD, that calculates the ‘integer modulo function’ then the predicate pair

    ≥ 0 ∧ b > 0, Post(z,a,b): z = a mod b

    a

    Pre(a,b):

    2nd Irish Workshop on Formal Methods, 19981

    下载Word文档免费下载:

    Declarative View of Imperative Programs Hugh下载

    (共21页)
  • 赵孟頫:书法大师是怎么炼成的? 2019-06-17
  • 工业互联网支持政策密集出台 2019-06-09
  • 强势发力体育营销 世界杯中国企业改变“旁观”窘状 2019-06-09
  • 小型地铺: 规模较小,中介费较实惠 2019-06-09
  • 以色列:卷入贪腐案  以总理接受警方调查 2019-06-09
  • 亳州留置“第一案”审理!谯城区一书记被指控 2019-06-08
  • 一周人事:国务院发布任免刘伟当选北京市总工会主席 2019-06-07
  • 【十九大·理论新视野】动漫:“社会主义现代化强国”如何建成 2019-06-07
  • 第530期:为何吃新鲜蔬果能抗肿瘤、强免疫……?因为有“它”! 2019-06-06
  • 贵州遵义:完善本土专技人才培养工程 2019-06-06
  • 太美了!合肥初雪航拍 看完想在雪地打滚 2019-06-05
  • 浙江省网络文明公益宣传创意作品展示 2019-06-05
  • 沈阳国际徒步日活动将于16日举行 超3万人参与 2019-06-04
  • 食品舆情:京东回应“假茅台”系被调包 饿了么推出可食用筷子宣传环保 2019-06-03
  • 青岛峰会为世界注入强大正能量(钟声) 2019-06-02
  • 美因茨大学格尔翻译学院 英国沃特福德市 psp大航海时代中文版 纽伦堡天气 广岛三箭vs柏太阳神直播 重庆时时彩推荐号码 巴萨VS比利亚雷亚尔 桑普多利亚球星 绝地求生刺激战场下载 卡利亚里桑普多利亚