跳过至内容[Spectre 文档](/)主菜单 [主页](/)[](https://github.com/spectrelang/spectre)外观[](https://github.com/spectrelang/spectre)菜单返回顶部侧边栏导航元信息- [安装](/installation.html)- [关于](/about.html)基础知识- [变量](/vars.html)- [类型](/types.html)- [函数](/functions.html)- [控制流](/control-flow.html)- [模式匹配](/pattern-matching.html)- [模块与导入](/modules-and-imports.html)- [错误处理](/error-handling.html)- [接口/规范](/specifications.html)- [泛型](/generics.html)- [类型参数约束](/type-argument-constraints.html)- [标签联合](/tagged-unions.html)契约式设计概念- [前置条件](/preconditions.html)- [后置条件](/postconditions.html)- [不变式](/invariants.html)- [断言](/assertions.html)- [信任传播](/trust-propagation.html)内置函数- [fmt](/fmt.html)- [len](/len.html)- [addr](/addr.html)- [deref](/deref.html)- [alloc](/alloc.html)- [free](/free.html)- [memcpy](/memcpy.html)- [memset](/memset.html)- [memmove](/memmove.html)- [puts](/puts.html)- [print](/print.html)- [zeroed](/zeroed.html)- [args](/args.html)- [bitcast](/bitcast.html)- [load](/load.html)- [load8](/load8.html)- [call](/call.html)- [snprintf](/snprintf.html)- [dprintf](/dprintf.html)- [reserve](/reserve.html)- [get](/get.html)- [insert](/insert.html)- [capacity](/capacity.html)- [ptradd](/ptradd.html)- [store](/store.html)- [store8](/store8.html)- [staticerror](/staticerror.html)- [flush](/flush.html)- [stdin](/stdin.html)- [stdout](/stdout.html)- [fgets](/fgets.html)- [atoi](/atoi.html)- [itoa](/itoa.html)本页内容# SpectreSpectre 是一种专为安全的、基于契约的底层系统编程而设计的编程语言。它支持类型级别的不变式以及函数级别的前置条件和后置条件并且默认通过不可变性来确保安全性。本文档旨在作为 Spectre 编程语言的用户指南。设计初衷目前缺乏能在底层强制保证正确性的基于契约的编程语言。Spectre 的设计理念是默认支持正确性、合理的数据流和不可变性从而使底层编程更安全同时又不影响语言及其工具链的便利性和开发体验。只要可能契约都会在编译时进行评估。不过为避免类似 Z3SMT 求解器等系统的复杂性以及编译器无法证明某些条件为真带来的不便那些无法在编译时评估的检查会自动在运行时执行。不过发布版本中运行时检查是否保留取决于是否使用了受保护的构造。为了保留底层控制权内存采用手动管理通常会使用标准库分配器如 Arena、Stack或自定义分配器。该语言可将高级代码编译为 QBE 中间表示IR然后进一步转换为特定平台的汇编代码。此外还有实验性的 LLVM 和 C99 后端。值得一提的是它有一个 –translate-c 特性能将 C 代码转换为等效的 Spectre 代码这对现有项目迁移到 Spectre 很有帮助。快速上手通过以下代码可以实现简单的 “Hello, world” 程序val std use(std)pub fn main() i32 {trust std.stdio.print(Hello, world: {d}., {10})return 0}你会注意到代码中使用了 trust 关键字。任何有底层不安全机制的操作如 IO 操作像 std.stdio.print 使用的 print 内置函数都必须显式使用 trust因为这些操作本质上是不纯的。不过如果你使用围绕这些函数的安全包装器使用前置条件、不变式等或者使用更简单的函数就无需这样做。例如对于简单的 puts 函数除非出现严重的内存不足OOM错误否则它不会失败所以在标准库中它被标记为安全的无需使用 trust。前言本文档可能会过时不保证能反映最新的 Spectre API。分页导航[下一页安装](/installation.html)
Spectre：支持编译时契约评估，可转换 C 代码的安全底层编程语言！
跳过至内容[Spectre 文档](/)主菜单 [主页](/)[](https://github.com/spectrelang/spectre)外观[](https://github.com/spectrelang/spectre)菜单返回顶部侧边栏导航元信息- [安装](/installation.html)- [关于](/about.html)基础知识- [变量](/vars.html)- [类型](/types.html)- [函数](/functions.html)- [控制流](/control-flow.html)- [模式匹配](/pattern-matching.html)- [模块与导入](/modules-and-imports.html)- [错误处理](/error-handling.html)- [接口/规范](/specifications.html)- [泛型](/generics.html)- [类型参数约束](/type-argument-constraints.html)- [标签联合](/tagged-unions.html)契约式设计概念- [前置条件](/preconditions.html)- [后置条件](/postconditions.html)- [不变式](/invariants.html)- [断言](/assertions.html)- [信任传播](/trust-propagation.html)内置函数- [fmt](/fmt.html)- [len](/len.html)- [addr](/addr.html)- [deref](/deref.html)- [alloc](/alloc.html)- [free](/free.html)- [memcpy](/memcpy.html)- [memset](/memset.html)- [memmove](/memmove.html)- [puts](/puts.html)- [print](/print.html)- [zeroed](/zeroed.html)- [args](/args.html)- [bitcast](/bitcast.html)- [load](/load.html)- [load8](/load8.html)- [call](/call.html)- [snprintf](/snprintf.html)- [dprintf](/dprintf.html)- [reserve](/reserve.html)- [get](/get.html)- [insert](/insert.html)- [capacity](/capacity.html)- [ptradd](/ptradd.html)- [store](/store.html)- [store8](/store8.html)- [staticerror](/staticerror.html)- [flush](/flush.html)- [stdin](/stdin.html)- [stdout](/stdout.html)- [fgets](/fgets.html)- [atoi](/atoi.html)- [itoa](/itoa.html)本页内容# SpectreSpectre 是一种专为安全的、基于契约的底层系统编程而设计的编程语言。它支持类型级别的不变式以及函数级别的前置条件和后置条件并且默认通过不可变性来确保安全性。本文档旨在作为 Spectre 编程语言的用户指南。设计初衷目前缺乏能在底层强制保证正确性的基于契约的编程语言。Spectre 的设计理念是默认支持正确性、合理的数据流和不可变性从而使底层编程更安全同时又不影响语言及其工具链的便利性和开发体验。只要可能契约都会在编译时进行评估。不过为避免类似 Z3SMT 求解器等系统的复杂性以及编译器无法证明某些条件为真带来的不便那些无法在编译时评估的检查会自动在运行时执行。不过发布版本中运行时检查是否保留取决于是否使用了受保护的构造。为了保留底层控制权内存采用手动管理通常会使用标准库分配器如 Arena、Stack或自定义分配器。该语言可将高级代码编译为 QBE 中间表示IR然后进一步转换为特定平台的汇编代码。此外还有实验性的 LLVM 和 C99 后端。值得一提的是它有一个 –translate-c 特性能将 C 代码转换为等效的 Spectre 代码这对现有项目迁移到 Spectre 很有帮助。快速上手通过以下代码可以实现简单的 “Hello, world” 程序val std use(std)pub fn main() i32 {trust std.stdio.print(Hello, world: {d}., {10})return 0}你会注意到代码中使用了 trust 关键字。任何有底层不安全机制的操作如 IO 操作像 std.stdio.print 使用的 print 内置函数都必须显式使用 trust因为这些操作本质上是不纯的。不过如果你使用围绕这些函数的安全包装器使用前置条件、不变式等或者使用更简单的函数就无需这样做。例如对于简单的 puts 函数除非出现严重的内存不足OOM错误否则它不会失败所以在标准库中它被标记为安全的无需使用 trust。前言本文档可能会过时不保证能反映最新的 Spectre API。分页导航[下一页安装](/installation.html)
