3.1 Data Type and Type Checking 数据类型与数据类型检验

本节目标

• 静态类型检查与动态类型检查 — static/dynamic type checking
• 可变数据类型与不可变数据类型 — mutable/immutable
• Snapshot图理解数据类型

1 Data type in programming languages

数据类型Type = 数据 + 操作 —— 类比抽象代数中群的定义，也是集合和集合上的二元运算。
变量Variable：用特定的数据类型定义，可以存储满足类型约束的值
对于Java：

• Primitive types 基本数据类型——int long boolean double char
• Object types 对象数据类型——String Integer
  
  Boxed primitives — 包装基本类型，将基本类型包装为对象类型，通常是在定义Collection时使用它们，是Immutable的，一般情况下不要使用，可以自动转换

2 Static/Dynamic data types

Java是一个静态类型语言，是在编译阶段进行类型检查的。而Python是动态类型检查的语言，是在运行阶段进行类型检查的。每一行没错的Python代码都是可以独立运行的。没错Python就是这么nice！还要什么Java

这里会有一个小疑问：为什么我们在Eclipse/IDEA等各种IDE中敲代码的时候，没有进行编译就有各种报错信息呢？这是因为你每敲出一个代码，它就会自动为你编译，所以我们能够实时的看到各种报错信息。不过这可能也是导致IDE吃内存的原因之一吧。其实我还怀疑过是Java也有解释器的原因…

3 Types checking

• 静态类型检查 — 在编译时检查，避免了将错误带入到运行阶段，可以提高程序的正确性/健壮性，它能够检查的错误有：

  • 语法错误
  • 类名/函数名错误
  • 参数数目/类型错误
  • 返回值类型错误 — like return “30”; from a function that’s declared to return an int
  • 总之，你在使用IDE时，没有运行前的所有IDE帮你报出的错误都是基于静态类型检查的。

• 动态类型检查 — 在运行时检查，它能够检查的错误有：

  • 非法的参数值
  • 非法的返回值 — when the specific return value can’t be represented in the type.
  • 越界
  • 空指针

• 无检查，直接报错
  综上，静态检查是关于“类型”的检查，不关心值；动态检查时关于“值”的检查

4 Mutability and Immutability

改变一个变量：将该变量指向另一个值的存储空间
改变一个变量的值：将该变量当前指向的值的存储空间中写入一个新的值

Immutability 不变性 — 重要的设计原则

Immutable types 不变数据类型，一旦被创建，其中的值不能被改变。如果是引用类型，也可以是不变的，一旦确定了指向的对象，指针就不能再改变。用final来声明，对final的变量检查在静态类型检查中执行

• final类无法派生子类
• final变量无法改变值/引用
• final方法无法被子类重写

一个不可变类型的对象不能修改其中的属性。以下用String结合代码快照图Snapshot来展现：

但是有一种可以改变其中值的String类型，StringBuilder！，同样的来看看快照图

那么有什么区别呢？反正最终内部的值还不是按照我们期望的那样改变了么。但是这是单引用的情况，如果我们有多个引用，那么情况将会变得不一样了。来看看下面这个快照

发现了问题的严重性：如果我们有多个引用指向同一个对象，那么当其中的一个引用修改了这个对象的内部值时，其他的所有引用所指向的值也同时发生了改变。

但是，使用不可变类型时，对其频繁修改会产生大量临时拷贝，需要较多的垃圾回收。可变类型就避免了这种情况。
所以，为什么我们需要不可变类型？所以要什么自行车？

安全！Java是作为一个面向对象语言来设计的，它与C类语言的不同点就是没有指针，更加安全。所以当我们设计软件时，要考虑“折中”

那么怎么避免过多的指向同一个对象的引用产生呢？想象一个场景，这里有一个类，这个类中的属性全都是private的。那么要如何查看这些属性呢？很自然的一个想法就是创建一个public的Observer，返回这个属性就好了。比如：

return this.field

好像没有什么不对。等一下！假设这个属性是Mutable的，这不就是相当于把引用暴露出来了么？用户如果修改了其中的内容，不安全因素就产生了！那么要怎么做呢？

Defensive copying 防御性拷贝——返回给用户一个全新的对象
但是如果你的对象是Immutable的，就不用提供防御性拷贝了

5 Snapshot diagram as a code-level, run-time, and moment view

偷点懒了，这些图不好画，就直接上PPT了

6 Complex data types: Arrays and Collections

7 Useful immutable types

NULL references

3.2 Designing Specification 设计规约

本节目标

• 理解Spec
• 前置条件/后置条件/precondition/post-condition
• 规约之外
• 陈述式、操作式规约
• 规约的强度及其比较
• 如何写出一个好的Spec

1 Functions & methods in programming languages

看一个具体的spec的例子

2 Specification：Programming for communication

Spec是一种客户端与程序员达成一种约定，双方都确定了各自的责任，程序员只负责spec要求中的部分——即完成了正确性的要求，至于spec之外的情况是健壮性的要求。而客户端只需要理解spec即可对程序进行正确调用。

只讲“能做什么”，不讲“怎么实现”
判断两个函数是否行为上等价，通过spec来判断，如果在spec的要求下，两个函数的行为相同，那么它们等价。

precondition前置条件