比浏览器更快的访问！
33 关系: Ada，库尔特·哥德尔，代码审查，形式化方法，形式验证，形式语义学，公理語義，图灵完全，程序，程序分析，美国食品药品监督管理局，生命攸關系統，目标代码，计算，计算机安全隐患，计算机科学，计算机程序，軟體度量，软件，软件测试，霍尔逻辑，阿隆佐·邱奇，艾伦·图灵，逆向工程，Lint，Polyspace，SPARK，抽象化 (計算機科學)，抽象释义，源代码，斷言 (程式)，操作语义学，数据流分析。
Ada
Ada，是一种程序设计语言。它源于美国军方的一个计划，旨在整合美军系统中运行着上百种不同的程序设计语言编写的程序，並提高除錯能力與效率，由Pascal及其他語言擴展而成，比較接近自然語言和數學表達式，並用「Ada」命名以紀念-zh-cn:埃达·洛夫莱斯;zh-tw:愛達·勒芙蕾絲;zh-hk:愛達·勒芙蕾絲;zh-sg:埃达·洛夫莱斯;-（Ada Lovelace）。.
新！!: 靜態程序分析和Ada · 查看更多 »
库尔特·哥德尔
库尔特·弗雷德里希·哥德尔（Kurt Friedrich Gödel，），出生於奧匈帝國的數學家、邏輯學家和哲學家，维也纳学派（维也纳小组）的成员。其最杰出的贡献是哥德尔不完备定理和连续统假设的相对协调性证明。.
新！!: 靜態程序分析和库尔特·哥德尔 · 查看更多 »
代码审查
代碼審查（Code review）是指對電腦源代码系統化地审查，常用的方式進行，其目的是在找出及修正在軟體開發初期未發現的錯誤，提升软件质量及開發者的技術。代碼審查常以不同的形式進行，例如结对编程、非正式的看過整個程式碼，或是正式的。.
新！!: 靜態程序分析和代码审查 · 查看更多 »
形式化方法
形式化方法，中文也稱形式方法、正規方法。在计算机科学和软件工程领域，形式化方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。将形式化方法用于软件和硬件设计，是期望能够像其它工程学科一样，使用适当的数学分析以提高设计的可靠性和強健性。但是，由于采用形式化方法的成本高意味着它们通常只用于开发注重安全性的高度整合的系统。.
新！!: 靜態程序分析和形式化方法 · 查看更多 »
形式验证
在计算机硬件（特别是集成电路）和软件系统的设计过程中，形式验证的含义是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。.
新！!: 靜態程序分析和形式验证 · 查看更多 »
形式语义学
在计算理论中，形式语义学是关注计算的模式和程序设计语言的含义的严格的数学研究的领域。 语言的形式语义是用数学模型去表达该语言描述的可能的计算来给出的。 形式语义学（formal semantics），是程序设计理论的组成部分，以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义，使语义形式化的学科。 提供程序设计语言的形式语义的方法很多，其中主要类别有：.
新！!: 靜態程序分析和形式语义学 · 查看更多 »
公理語義
#重定向 公理语义学.
新！!: 靜態程序分析和公理語義 · 查看更多 »
图灵完全
#重定向 圖靈完備性.
新！!: 靜態程序分析和图灵完全 · 查看更多 »
程序
程序（procedure），指特定的一系列動作、行動或操作，而這些活動、動作或操作必須以相同方式執行，藉此在相同環境下恆常得出相同的結果（例如緊急應變程序）。粗略而言，程序可以指一序列的活動、作業、步驟、決斷、計算和工序，當它們保證依照嚴格規定的順序發生時即產生所述的後果、產品或局面。一個程序通常引致一個改變。現在小孩也可以寫程式。.
程序分析
程序分析技术包括静态程序分析和动态分析技术。静态分析，如控制流分析、数据流分析、、等。动态分析包括等。 *.
新！!: 靜態程序分析和程序分析 · 查看更多 »
美国食品药品监督管理局
美国食品药品监督管理局（U.S. Food and Drug Administration，缩写为FDA）为美國衛生及公共服務部直轄的联邦政府机构，其主要职能为负责对美国国内生产及进口的食品、膳食补充剂、药品、疫苗、生物医药制剂、血液制剂、医疗设备、放射性设备、兽药和化妆品进行监督管理，同时也负责执行公共健康法案（the Public Health Service Act）的第361号条款，包括公共卫生条件及州际旅行和运输的检查、对于诸多产品中可能存在的疾病的控制等等。.
新！!: 靜態程序分析和美国食品药品监督管理局 · 查看更多 »
生命攸關系統
生命攸關系統（life-critical system）或安全攸關系統（safety-critical system）也稱為生命關鍵系統或安全關鍵系統，是指若系統失效或誤動作，會產生以下後果的系統：.
新！!: 靜態程序分析和生命攸關系統 · 查看更多 »
目标代码
标代码（object code）指计算机科学中编译器或汇编器处理源代码后所生成的代码，它一般由机器代码或接近于机器语言的代码组成。目标文件（object file）即存放目标代码的计算机文件，它常被称作二进制文件（binaries）。 目标文件包含着机器代码（可直接被计算机中央处理器执行）以及代码在运行时使用的数据，如重定位信息，如用于链接或调试的程序符号（变量和函数的名字），此外还包括其他调试信息。目标文件是从源代码文件产生程序文件这一过程的中间产物，链接器正是通过把目标文件链接在一起来生成可执行文件或库文件。目标文件中唯一的要素是机器代码，例如，用于嵌入式系统的目标文件可能仅仅含有机器代码。.
新！!: 靜態程序分析和目标代码 · 查看更多 »
计算
計算（Calculation）是一種將「單一或多個的輸入值」轉換為「單一或多個的結果」的一種思考過程。 計算的定義有許多種使用方式，有相當精確的定義，例如使用各種算法進行的「算术」，也有較為抽象的定義，例如在一場競爭中「策略的計算」或是「計算」兩人之間關係的成功機率。 將7乘以8（7x8）就是一種簡單的算術。 利用布莱克-斯科尔斯模型（Black-Scholes Model）來算出財務評估中的公平價格（fair price）就是一種複雜的算術。 從投票意向計算評估出的選舉結果（民意調查）也包含了某種算術，但是提供的結果是「各種可能性的範圍」而不是單一的正確答案。.
计算机安全隐患
计算机安全隐患（Vulnerability），俗称安全漏洞（Security hole），指计算机系统安全方面的缺陷，使得系统或其应用数据的保密性、完整性、可用性、访问控制和监测机制等面临威胁。 许多安全漏洞是程序错误导致的，此时可叫做（Security bug），但并不是所有的安全隐患都是程序安全错误导致的。.
新！!: 靜態程序分析和计算机安全隐患 · 查看更多 »
计算机科学
计算机科学用于解决信息与计算的理论基础，以及实现和应用它们的实用技术。 计算机科学（computer science，有时缩写为CS）是系统性研究信息与计算的理论基础以及它们在计算机系统中如何与应用的实用技术的学科。 它通常被形容为对那些创造、描述以及转换信息的算法处理的系统研究。计算机科学包含很多分支领域；有些强调特定结果的计算，比如计算机图形学；而有些是探討计算问题的性质，比如计算复杂性理论；还有一些领域專注于怎样实现计算，比如程式語言理論是研究描述计算的方法，而程式设计是应用特定的程式語言解决特定的计算问题，人机交互则是專注于怎样使计算机和计算变得有用、好用，以及随时随地为人所用。 有时公众会误以为计算机科学就是解决计算机问题的事业（比如信息技术），或者只是与使用计算机的经验有关，如玩游戏、上网或者文字处理。其实计算机科学所关注的，不仅仅是去理解实现类似游戏、浏览器这些软件的程序的性质，更要通过现有的知识创造新的程序或者改进已有的程序。 尽管计算机科学（computer science）的名字里包含计算机这几个字，但实际上计算机科学相当数量的领域都不涉及计算机本身的研究。因此，一些新的名字被提议出来。某些重点大学的院系倾向于术语计算科学（computing science），以精确强调两者之间的不同。丹麦科学家Peter Naur建议使用术语"datalogy"，以反映这一事实，即科学学科是围绕着数据和数据处理，而不一定要涉及计算机。第一个使用这个术语的科学机构是哥本哈根大学Datalogy学院，该学院成立于1969年，Peter Naur便是第一任教授。这个术语主要被用于北欧国家。同时，在计算技术发展初期，《ACM通讯》建议了一些针对计算领域从业人员的术语：turingineer，turologist，flow-charts-man，applied meta-mathematician及applied epistemologist。 三个月后在同样的期刊上，comptologist被提出，第二年又变成了hypologist。 术语computics也曾经被提议过。在欧洲大陆，起源于信息（information）和数学或者自动（automatic）的名字比起源于计算机或者计算（computation）更常见，如informatique（法语），Informatik（德语），informatika（斯拉夫语族）。 著名计算机科学家Edsger Dijkstra曾经指出：“计算机科学并不只是关于计算机，就像天文学并不只是关于望远镜一样。”（"Computer science is no more about computers than astronomy is about telescopes."）设计、部署计算机和计算机系统通常被认为是非计算机科学学科的领域。例如，研究计算机硬件被看作是计算机工程的一部分，而对于商业计算机系统的研究和部署被称为信息技术或者信息系统。然而，现如今也越来越多地融合了各类计算机相关学科的思想。计算机科学研究也经常与其它学科交叉，比如心理学，认知科学，语言学，数学，物理学，统计学和经济学。 计算机科学被认为比其它科学学科与数学的联系更加密切，一些观察者说计算就是一门数学科学。 早期计算机科学受数学研究成果的影响很大，如Kurt Gödel和Alan Turing，这两个领域在某些学科，例如数理逻辑、范畴论、域理论和代数，也不断有有益的思想交流。.
新！!: 靜態程序分析和计算机科学 · 查看更多 »
计算机程序
计算机程序（Computer Program）是指一组指示计算机或其他具有訊息处理能力装置每一步动作的指令，通常用某种程序设计语言编写，运行于某种目标体--结构上。打个比方，一个程序就像一个用汉语（程序设计语言）写下的红烧肉菜谱（程序），用于指导懂汉语（編譯器）同時也會烹饪手法的人（体--结构）来做这道菜。 通常，以英文文本為基礎的计算机程序要经过編譯和連結而成为一种人们不易看清而计算机可解讀的一連串數字的格式，然后放入运行。未经编译就可运行的程序，通常称之为脚本程序（script）。.
新！!: 靜態程序分析和计算机程序 · 查看更多 »
軟體度量
軟體度量（software metric）是一個對於軟體性質及其規格的量測。軟體度量的目的是獲得客觀、可以複製及量化的量測結果，依軟體度量性質及特性的不同，可以分別應用在軟體開發的時程及預算規劃、成本估算、品質保證測試、軟體偵錯、軟體性能最佳化或專案人員配置的最佳化等領域。.
新！!: 靜態程序分析和軟體度量 · 查看更多 »
软件
軟體（software）是一系列按照特定顺序组织的電腦数据和指示，是電腦中的非有形部分。電腦中的有形部分稱為硬體，由電腦的外殼及各零件及電路所組成。電腦軟體需有硬體才能運作，反之亦然，軟體和硬體都無法在不互相配合的情形下進行實際的運作。 一般来說，计算机软件划分为程式語言、系统软件、应用软件和介于这两者之间的中介軟體。其中系统软件为计算机使用提供最基本的功能，但是并不针对某一特定应用领域。而应用软件则恰好相反，不同的应用软件根据用户和所服务的领域提供不同的功能。 软件包括所有在電腦執行的程式，和其架構無關，例如執行檔、函式庫及腳本語言都屬於软件。軟體不分架構，有其共通的特性，在執行後可以讓硬體執行依設計時要求的機能。軟體儲存在記憶體中，軟體不是可以碰觸到的實體，可以碰觸到的都只是儲存軟體的零件（記憶體）或是媒介（光碟或磁片等）。 软件并不一定只包括可以在计算机上运行的電腦程式，有些定義中，与電腦程式相关的文档，一般也被认为是软件的一部分。简单的说软件就是程式加文档的集合体。软件被应用于世界的各个领域，对人们的生活和工作都产生了深远的影响。.
软件测试
軟體測試（software testing），描述一種用來促進鑑定軟體的正確性、完整性、安全性和品質的過程。據此，您可能會想，軟體測試永遠不可能完整的確立任意電腦軟體的正確性。然而，在可計算理論（計算機科學的一個支派）一個簡單的數學證明推斷出下列結果：不可能完全解決所謂「當機」，指任意電腦程式是否會進入無窮迴圈，或者罷工並產生輸出問題。換句話說，軟體測試是一種實際輸出與預期輸出間的稽核或者比較過程。 软件测试的经典定义是：在规定的条件下对程序进行操作，以发现程序错误，衡量軟體品質，并对其是否能满足设计要求进行评估的过程。 軟體測試有許多方法，但對複雜的產品執行有效測試不僅僅是研究過程，更是創造並嚴格遵守某些呆板步驟的大事。測試的其中一個定義：為了評估而質疑產品的過程；這裡的“質疑”是測試員試著對產品做的事，而產品以測試者腳本行為反應作為回答。雖然大部分測試的智力過程不外乎回顧、檢查，然而「測試」這個词意味著產品動態分析──讓產品流暢運行。程式品質可能，而且通常會，隨系統不同而有差異；不過某些公認特性是共通的：可靠性、穩定性、輕便性、易於維護、以及實用性。請參照至ISO標準ISO 9126有更詳盡的說明。.
新！!: 靜態程序分析和软件测试 · 查看更多 »
霍尔逻辑
霍爾邏輯（Hoare Logic），又稱弗洛伊德-霍爾邏輯（Floyd–Hoare logic），是英国计算机科学家東尼·霍爾开发的形式系统，这个系统的用途是为了使用严格的数理逻辑推理來替计算机程序的正确性提供一组逻辑规则。 這個想法起源於罗伯特·弗洛伊德於較早的研究，他为流程图提供了类似的系统。東尼·霍爾於1969年首次發表，随后为其他研究者所精制。.
新！!: 靜態程序分析和霍尔逻辑 · 查看更多 »
阿隆佐·邱奇
阿隆佐·邱奇（Alonzo Church，）是美国数学家，1936年发表可计算函数的第一份精确定义，对算法理论的系统发展做出巨大贡献。邱奇在普林斯顿大学受教并工作四十年，曾任数学与哲学教授。1967年迁往加利福尼亚大学洛杉矶分校。 解决算法问题包括构造一个能解决某一指定集及其他相关集的算法，如果该算法无法构建，则表明该问题是不可解的。证明此种问题不可解性的定理是算法理论中的一大突破，邱奇的算法即为该类算法的首例。邱奇证明了基本几何问题的算法不可解性。同时证明了一阶逻辑中真命题全集的解法问题是不可解的。.
新！!: 靜態程序分析和阿隆佐·邱奇 · 查看更多 »
艾伦·图灵
艾伦·麦席森·图灵，OBE，FRS（Alan Mathison Turing，又译阿兰·图灵，Turing也常翻譯成--林或者杜林，）是英国計算機科學家、数学家、邏輯學家、密码分析学家和理论生物学家，他被视为计算机科学與人工智慧之父。 在第二次世界大战期间，图灵曾在“政府密码学校”（GC&CS，今政府通信总部）工作。政府密码学校位于布萊切利園，是英国顶级机密情报机构。图灵在这里从事密码破译工作，有一段时间，他领导了（Hut 8）小组，负责德国海军密码分析。 期间他设计了一些加速破译德国密码的技术，包括改进波兰战前研制的机器，一种可以找到恩尼格玛密码机设置的机电机器。 图灵在破译截获的编码信息方面发挥了关键作用，使盟军能够在包括大西洋战役在内的许多重要交战中击败纳粹，并因此帮助赢得了战争。 图灵对于人工智能的发展有诸多贡献，例如图灵曾写过一篇名为《》的论文，提問「机器会思考吗？」（Can Machines Think?），作為一种用于判定机器是否具有智能的测试方法，即图灵测试。至今，每年都有试验的比赛。此外，图灵提出的著名的图灵机模型为现代计算机的逻辑工作方式奠定了基础。 图灵是著名的男同性恋者，并因为其性倾向而遭到当时的英国政府迫害，职业生涯尽毁。他亦患有花粉过敏症。 图灵还是一位世界级的长跑运动员。他的马拉松最好成绩是2小時46分03秒（手動計時），比1948年奥林匹克运动会金牌成绩慢11分钟。1948年的一次跨国赛跑比赛中，他跑赢了同年奥运会银牌得主。.
新！!: 靜態程序分析和艾伦·图灵 · 查看更多 »
逆向工程
逆向工程，又称反向工程，是一种技术过程，即对一项目标产品进行逆向分析及研究，从而演绎并得出该产品的处理流程、组织结构、功能性能规格等设计要素，以制作出功能相近，但又不完全一样的产品。逆向工程源于商业及军事领域中的硬件分析。其主要目的是，在無法轻易获得必要的生产信息下，直接从成品的分析，推导产品的设计原理。 逆向工程可能会被误认为是对知识产权的严重侵害，但是在实际应用上，反而可能会保护知识产权所有者。例如在集成电路领域，如果怀疑某公司侵犯知识产权，可以用逆向工程技术来寻找证据。.
新！!: 靜態程序分析和逆向工程 · 查看更多 »
Lint
在電腦科學中，lint是一種工具程式的名稱，它用來標記原始碼中，某些可疑的、不具結構性（可能造成bug）的段落。它是一種靜態程序分析工具，最早適用於C語言，在UNIX平台上開發出來。後來它成為通用術語，可用於描述在任何一種電腦程式語言中，用來標記原始碼中有疑義段落的工具。.
新！!: 靜態程序分析和Lint · 查看更多 »
Polyspace
Polyspace是靜態程序分析的工具，利用抽象释义的方式進行大規模的分析，可以偵測C語言、C++或是Ada程式的原始碼中，是否有特定類型的執行期錯誤，或是證明沒有這類的錯誤。此工具也可以檢查原始碼是否符合特定的代碼標準。.
新！!: 靜態程序分析和Polyspace · 查看更多 »
SPARK
SPARK是一种安全的、经正式定义的编程语言。它被设计用来支持一些安全或商业集成为关键因素的应用软件的设计。SPARK有基于Ada 83和Ada 95的版本。最新版本RavenSPARK包含了Ravenscar Tasking Profile来支持高度集成应用中的同步。SPARK的正式和明确的定义使得多种静态分析技术在SPARK源代码的应用中成为可能。.
新！!: 靜態程序分析和SPARK · 查看更多 »
抽象化 (計算機科學)
在计算机科學中，抽象化（Abstraction）是將資料與程序，以它的語意來呈現出它的外觀，但是隱藏起它的實作細節。抽象化是用來減少程式的複雜度，使得程式設計師可以專注在處理少數重要的部份。一個電腦系統可以分割成幾個抽象層（Abstraction layer），使得程式設計師可以將它們分開處理。.
新！!: 靜態程序分析和抽象化 (計算機科學) · 查看更多 »
抽象释义
在计算机科学中，抽象释义是基于在有序集合特别是格上的单调函数，计算机程序的语义的可靠逼近理论。它可以被看作对计算机程序的部分执行，获取关于它的语义信息(比如，控制结构、信息流)而不进行所有计算。 它的主要具体应用是形式静态分析，关于计算机程序的可能执行的信息的自动提取；比如这种分析有两个主要用途.
新！!: 靜態程序分析和抽象释义 · 查看更多 »
源代码
源代码（Source code），也称源程序，是指一系列人类可读的计算机语言指令。 在现代程序语言中，源代码可以是以书籍或者磁带的形式出现；但最常用的格式是文本文件，这种典型格式的目的是为了编译出计算机程序。计算机源代码的最终目的是将人类可读的文本翻译成为计算机可以执行的二进制指令，这种过程叫做编译，通过编译器完成。.
新！!: 靜態程序分析和源代码 · 查看更多 »
斷言 (程式)
在程式設計中，斷言（assertion）是一種放在程式中的一階邏輯（如一個結果為真或是假的邏輯判斷式），目的是為了標示與驗證程式開發者預期的結果－當程式執行到斷言的位置時，對應的斷言應該為真。若斷言不為真時，程式會中止執行，並給出錯誤訊息。 例如，以下的程式包括二個斷言： x.
新！!: 靜態程序分析和斷言 (程式) · 查看更多 »
操作语义学
操作语义学是计算机科学中的一个概念，它是使得计算机程序在数学上更加严谨的一种手段。其它类似的手段包括提供形式语义学，包括公理语义学和指称语义。 一个计算机语言的操作语义描述一段合理的程序是怎样被理解为一系列计算机步骤的。这些步骤就是这个程序的意义。在函數程式語言中一段终结性的序列在最后一步的返回程序的值。（由于一个程序可能是非非決定的，一般来说一个程序能够有许多不同的计算步骤和许多不同的返回值。） 操作语义最早被用来定义Algol 68的语义。下面这句话引用修正的ALGOL 68报告： 一个使用严格语言编写的程序的意义是通过一个假设的计算机来执行该程序的组成部分时完成的行动来解释的。（Algol68，第二章） 丹纳·司科特是第一个在今天的这个定义下使用操作语义这个概念的（Plotkin04b）。以下是司科特关于形式语义学的讲稿，其中他提到了语义的“操作”观点。 把目光注意使得语义在更‘抽象’和更‘清晰’可以，但是假如把操作方面完全忽略的话这个计划毫无用处。（Scott70）.
新！!: 靜態程序分析和操作语义学 · 查看更多 »
数据流分析
数据流分析 是一种用于收集计算机程序在不同点计算的值的信息的技术。一个程序的控制流图(control flow graph, CFG)被用来确定对变量的一次赋值可能传播到程序中的哪些部分。这些信息通常被编译器用来优化程序。数据流分析的一个典型的例子就是可到达定义的计算。 进行数据流分析的最简单的一种形式就是对控制流图的某个节点建立数据流方程，然后通过迭代计算，反复求解，直到到达不动点。这种一般的方法是由Gary Kildall在Naval Postgraduate School讲课时发明的。.
新！!: 靜態程序分析和数据流分析 · 查看更多 »
