形式化方法

一、定义

形式化方法是一套基于严格数学逻辑、符号演算的软件开发与验证技术，用无歧义的数学语言描述系统需求、模型、代码行为，代替自然语言（自然语言存在模糊、二义性），可做自动化推导、证明、校验，从源头减少逻辑漏洞、并发 bug、安全缺陷。

二、落地到JAVA

Java 本身是编程语言，Java 中的形式化方法 = 用形式化工具 / 逻辑对 Java 程序做建模、规约、验证，核心场景：高可靠软件（航空、金融、车载、安全加密）。
1. 形式化规约（给 Java 程序写数学规范）
用专用形式语言定义类、方法的前置条件、后置条件、不变量，规定代码合法输入、输出结果、对象状态约束。
2. 形式化验证（证明 Java 代码符合规约）
基于 JML 等形式规约，自动化数学证明 Java 程序不存在：
数组越界、空指针、除零异常；
循环死循环、并发竞态条件；
业务逻辑违背需求；
常用工具：OpenJML、KeY、ESC/Java2。
3. 形式化建模（抽象 Java 系统）
用形式化语言（如 B 方法、Z 语言、Event-B）先搭建系统数学模型，再自动生成 / 转化为 Java 代码，保证代码和模型严格一致。

三、核心特点（Java 场景）
无歧义：全部使用一阶逻辑、集合、谓词数学表达，不存在文字理解偏差；
可机器自动校验：不像单元测试只能测少量用例，形式化证明覆盖所有合法输入；
嵌入 Java 生态：以注释扩展（JML）为主，兼容标准 Java，无需新编程语言；
高可靠性刚需：普通业务开发很少用，军工、轨道交通、支付安全、操作系统内核 Java 模块强制使用。
四、和普通测试的区别
单元测试：跑有限用例，只能证明有错，不能证明无错；
Java 形式化方法：数学全域证明，严格证明程序在全部合法输入下均正确。

Java的反射机制

一、什么是反射
反射（Reflection）：Java 在运行时获取类的完整信息（类名、属性、方法、构造器），并能动态创建对象、调用方法、读写成员变量的机制。
正常编码是正向操作：编译期直接 new 类()、调用方法；
反射是反向操作：运行时拿到 Class 对象，逆向解析类结构，实现动态编程。
核心：运行时获取类元数据，无视访问权限。
二、反射核心入口：Class 类
java.lang.Class 是反射的根，每个类在 JVM 中只会生成唯一 Class 对象，代表该类型。
获取 Class 对象的 3 种方式
// 1. 类名.class（编译期，推荐，不初始化类）
Class<User> clazz1 = User.class;

// 2. 对象.getClass()（已有实例时）
User user = new User();
Class<?> clazz2 = user.getClass();

// 3. Class.forName("全类名")（运行时动态加载，会执行静态代码块）
Class<?> clazz3 = Class.forName("com.demo.User");
三、反射核心四大组件
Class：类本身元信息
Constructor：构造器，反射创建对象
Method：方法，反射调用
Field：成员变量，反射读写值
四、完整反射示例
1. 实体类（含私有构造、私有属性、私有方法）
public class User {
    // 私有成员
    private String name;
    public int age;

    // 无参私有构造
    private User() {}
    // 公有有参构造
    public User(String name, int age) {
        this.name = name;
        this.age = age;
    }

    // 私有方法
    private void sayHello(String msg) {
        System.out.println("私有方法输出：" + msg + "，姓名：" + name);
    }
}
2. 反射完整操作代码
import java.lang.reflect.Constructor;
import java.lang.reflect.Field;
import java.lang.reflect.Method;

public class ReflectDemo {
    public static void main(String[] args) throws Exception {
        // 1. 获取Class对象
        Class<User> clazz = User.class;

        // ========== 1. 通过构造器创建对象 ==========
        // ① 公有构造创建对象
        Constructor<User> publicCon = clazz.getConstructor(String.class, int.class);
        User user = publicCon.newInstance("张三", 20);

        // ② 私有构造创建对象（必须暴力放开权限）
        Constructor<User> privateCon = clazz.getDeclaredConstructor();
        privateCon.setAccessible(true); // 暴力反射，忽略private
        User user2 = privateCon.newInstance();

        // ========== 2. 反射操作成员变量Field ==========
        // 读取私有name
        Field nameField = clazz.getDeclaredField("name");
        nameField.setAccessible(true);
        // 设置值
        nameField.set(user, "李四");
        // 获取值
        String nameVal = (String) nameField.get(user);
        System.out.println("反射获取私有name：" + nameVal);

        // 公有age无需setAccessible
        Field ageField = clazz.getField("age");
        ageField.set(user, 22);
        System.out.println("age：" + ageField.get(user));

        // ========== 3. 反射调用私有方法Method ==========
        Method sayMethod = clazz.getDeclaredMethod("sayHello", String.class);
        sayMethod.setAccessible(true);
        // 调用方法：invoke(对象实例, 方法参数)
        sayMethod.invoke(user, "测试反射调用");
    }
}
关键方法说明
setAccessible(true)
暴力反射开关，绕过 Java 访问权限校验（private/protected 都能操作）。
newInstance()
Constructor 对象调用，实例化对象；JDK9 废弃 clazz.newInstance()。
method.invoke(obj, args...)
执行方法：
普通方法：传入实例对象
静态方法：第一个参数传 null
五、反射优缺点
优点
动态灵活：运行时决定创建哪个类、调用哪个方法，框架底层核心。
解耦：配置文件 + 反射，不用硬编码 new 对象。
缺点
性能差：反射绕过编译期优化，大量反射会拖慢程序。
破坏封装：setAccessible(true) 强制访问私有成员，违背面向对象封装。
安全隐患：可绕过权限修改私有字段、执行私有方法；高安全场景禁用。
代码可读性差：大量异常捕获、字符串类名 / 方法名，容易写错。
六、反射典型应用场景
Spring IoC 容器：读取 xml / 注解，反射创建 Bean 对象、依赖注入
MyBatis：反射实例化实体类、给实体属性赋值（数据库映射）
单元测试 JUnit：反射调用 @Test 测试方法
序列化 / 反序列化（JSON 工具 Fastjson/Gson）：反射读写实体字段
动态代理（AOP 面向切面编程）底层依赖反射
七、反射与泛型、类型擦除
Java 泛型编译后会类型擦除，反射运行时看不到泛型约束：
List<String> list = new ArrayList<>();
Class<?> listCls = list.getClass();
// 运行时获取不到String，只能拿到ArrayList
System.out.println(listCls.getName());
如需获取泛型真实类型，使用 ParameterizedType。
八、安全关闭暴力反射
高版本 JDK 增加模块访问控制，默认不允许暴力反射操作内部类；可通过 JVM 参数开放权限，生产环境不建议随意开启。