Keywords

1 Introduction

This paper aims to provide a non-technical overview of Jifeng He’s main academic achievements during his career, as well as a chronological account of his main affiliations. Subsection 1.1 provides a brief overall biography and Subsect. 1.2 describes some early practical contributions in China. Section 2 covers his research at the University of Oxford in the United Kingdom, especially in collaboration with Tony Hoare. He then moved to the United Nations University in Macau, as reported in Sect. 3. Latterly until his retirement, he was based at the East China Normal University in Shanghai, as described in Sect. 4. The paper concludes with an overall appreciation of his achievements in Sect. 5. Overall, this paper provides a personal reflection of the authors in their collaboration with Jifeng over the years.

1.1 Brief Biography

Jifeng He was born in Shanghai China, in August 1943. He graduated in 1965 from the Department of Mathematics at Fudan University, located in Shanghai. Since 1965, he has held a position at East China Normal University (ECNU) in Shanghai, successively serving as a teaching assistant and then lecturer, and was promoted to full professor in 1986. In 1988, he was awarded the title of National Young and Middle-aged Experts with Outstanding Contributions. From 1980 to 1981, he was a visiting scholar at Stanford University and the University of San Francisco in California, United States. From 1983 to 1998, he worked as a senior researcher in the Programming Research Group (PRG) at the Oxford University Computing Laboratory (OUCL) in the United Kingdom, collaborating extensively with Tony Hoare [54], based in Oxford although retaining his position at ECNU. He was an important researcher on the European ProCoS project from 1989.

From 1998, Jifeng worked as a senior researcher at the International Institute of Software Technology of the United Nations University (UNU/IIST) in Macau. During 2002 to 2019, he was the Dean of the Software Engineering Institute at East China Normal University. In 2002, he joined the first group of lifelong professors of East China Normal University. He was elected in 2005 as an academician of the Chinese Academy of Sciences, the highest scientific recognition in China. He received an honorary doctorate from the University of York (UK) in 2009. In December 2015, he was awarded the French National Palm Education Knight Medal. From 2017, Jifeng started to consider the issues around trustworthiness in Artificial Intelligence (AI). In 2019, Jifeng was appointed as the Distinguished Professor at Tongji University located in Shanghai. Jifeng’s research interests have included sound methods for the specification of computer systems, communications, applications, and standards, as well as techniques for designing and implementing those specifications in software and/or hardware with high reliability.

This paper provides a non-technical overview of Jifeng’s academic achievements. More technical details related to some of his contributions are available elsewhere in this volume [59, 63, 71].

Fig. 1.
figure 1

Jifeng He speaking at a BCS-FACS event in London, 2018. (See also Fig. 3.)

Full size image

1.2 Practical Contributions

This paper is mainly about the theoretical contributions of Jifeng at Oxford, UNU/IIST, and ECNU. It should be noted that Jifeng also has made remarkable practical contributions. In 1982, Jifeng led a team to undertake one of the 38 major scientific and technological research projects of the State Council in China, the Office Chinese Character Information Processing System, whose core technology was the independent self-development of China’s first Chinese Character Relational Database System (ECNIS), which provided a practical Chinese character information processing platform for China’s “paperless” office. It was widely used in the field of office work by various domestic institutions at that time. The scientific research achievements won the first prize of the Shanghai Excellent Software Award in 1985 and the Outstanding Scientific and Technological Achievements Award of the National Education Commission in 1986.

2 University of Oxford

From 1983 to 1998, Jifeng worked as a senior researcher (a “Senior Research Officer”) in the Programming Research Group (PRG) at the Oxford University Computing Laboratory (OUCL) in the UK. He mainly collaborated with the leader of the PRG, Tony Hoare, who invited him to come to Oxford during a visit to China. Although Jifeng retained his position at East China Normal University during this time, he spent most of his time working as a researcher in Oxford, mainly with Tony Hoare. From 1989, he was a significant contributor on the European ProCoS project concerning “Provably Correct Systems”, instigated by Tony Hoare and others.

Before the ProCoS project, Jifeng collaborated with Tony Hoare on research concerning the “weakest prespecification”, generalizing the concept of Edsger Dikstra’s weakest precondition. This was first published as a PRG Technical Monograph in 1985 [44], then as two related journal papers in 1986 [45, 46], and also as a shorter summary journal paper in 1987 [52]. Later they collaborated with Jeff Sanders on data refinement [27] and prespecification for such refinement [48]. Jifeng was also a coauthor of the highly cited 1987 Laws of Programming paper by Tony Hoare et al. [51], presenting a complete set of algebraic laws for Edsger Dijkstra’s nondeterministic sequential programming language.

2.1 Provably Correct Systems (“ProCoS”)

From 1989, Tony Hoare led the ProCoS “Basic Research Action” (ESPRIT BRA 3104) project on Provably Correct Systems with European partners in Denmark (under Dines Bjørner) and Germany (under Hans Langmaack and also Ernst-Rüdiger Olderog), as well as in the UK (initially with Cliff Jones and also Ursula Martin) [1]. This ran in parallel with the UK Information Engineering Directorate (IED) SAFEMOS project in “Totally Verified Systems” with the University of Cambridge (under Mike Gordon), SRI Cambridge (under Roger Hale), and INMOS (under David May and David Shepherd) [2, 10]. Subsequently, the ProCoS II project [15] and the ProCoS-WG Working Group continued the work of ProCoS in the 1990s [16]. Jifeng He was a key researcher involved with ProCoS, especially working on program compilation aspects of the project, and collaborated on tutorials about the project [14]. Ultimately, this work led to his important ideas on Unifying Theories of Programming, as described later in Subsect. 2.2.

Verifiable Compiling Specification: The ProCoS project studied verifying computer-based systems from requirements through to programming and compilation. Initial research considered an algebraic approach to the verifiable compiling specification and prototyping of the ProCoS level 0 programming language, based on a subset of the Occam programming language [47], with prototyping using logic programming in Prolog by Jonathan Bowen [12], based on a shallow embedding approach [7]. Later, recursion was also considered [23]. This approach was further developed to cover the specification, verification, and prototyping of an optimized compiler [25]. Jifeng also collaborated with Tony Hoare and Augusto Sampaio on a normal-form approach to compiler design [50]. In 1994, Jifeng published a complete book on provably correct systems, covering the modelling of communication languages and the design of optimized compilers [21].

Real-time Systems: Later work on ProCoS by Jifeng He and others considered a time interval semantics and the implementation of a real-time programming language [24]. Further work covered hybrid parallel programming and the implementation of synchronised communication [20]. Jifeng collaborated with Roger Hale on the SAFEMOS project concerning a real-time programming language [19]. He also undertook research with others, including Hussein Zedan, on real-time refinement [65], a predictive semantics for the refinement of real-time systems [64], and a specification-oriented semantics for real-time system refinement [66].

Hardware Compilation: Ian Page and Wayne Luk at Oxford introduced ideas of compiling an Occam-like programing language including parallelism directly into hardware for implementation as a netlist of gate-level components on a Field-Programmable Gate Array (FPGA) chip. These ideas were adopted on the ProCoS project, including by Jifeng. Initial ideas were published in a highly cited conference paper on a provably correct hardware implementation of the Occam programming language [28], led by Jifeng in collaboration with Ian Page and Jonathan Bowen. This work was also undertaken collaboratively as part of the SAFEMOS project by Jonathan Bowen et al. [11] and with Jianping Zheng, using a simulation approach for provably correct hardware compilation [39]. Further papers on the specification and verification of a hardware compilation scheme [8] and an algebraic approach to hardware compilation [9] appeared later.

2.2 Unifying Theories of Programming (UTP)

Starting during ProCoS, for example in considering the connection between algebraic and operational semantics [26], and continuing afterwards, Jifeng collaborated with Tony Hoare on their magnum opus Unifying Theories of Programming (UTP), published in 1998 [49]. An associated paper was presented at the 4th International Seminar on Relational Methods in Computer Science (RelMiCS) [32]. UTP considers the challenge of connecting different forms of semantics. For example, it is possible to link algebraic, denotational, and operational semantics, including demonstrating their equivalence. In parallel, Jifeng also collaborated on highly cited work with Karen Seidel and Annabelle McIver on probabilistic models for the Guarded Command Language (GCL) [36], with Qiwen Xu and Willem-Paul de Roever on the rely-guarantee method for verifying shared variable concurrent programs [72], and with Tony Hoare on a trace model for pointers and objects [53].

The UTP book has spawned a community of researchers, including a regular UTP symposium. Jifeng [22] and Tony Hoare [62] were later both keynote presenters at the UTP 2016 Symposium in Reykjavik, Iceland [17]. It is interesting to consider papers connected to UTP, using the visual representation provided by the Connected Papers website (https://connectedpapers.com). It can be noted that Jim Woodcock is a major contributor of UTP papers, together with his collaborator Ana Cavalcanti, both at the University of York. They have developed Circus, an integration of the formal notations of Z, CSP, and Carroll Morgan’s refinement calculus, underpinned by UTP, as described elsewhere in this volume [71].

3 United Nations University

In 1998, the year of publication of the Unifying Theories of Programming book with Tony Hoare [49], Jifeng took up a position with United Nations University International Institute of Software Technology (UNU/IIST) in Macau as a senior researcher. UNU/IIST was initially established under the leadership of Dines Bjørner, who headed the Danish partner on the ProCoS project, the Technical University of Denmark. In this section, we consider some important contributions of Jifeng during his time at UNU/IIST.

Verilog Hardware Description Language: Modern hardware design typically uses a Hardware Description Language (HDL) to express designs at various levels of abstraction. An HDL is a high-level programming language, with usual programming constructs such as assignments, conditionals, and iterations, together with appropriate extensions for real-time, concurrency and data structures suitable for modelling hardware. Verilog is an HDL that has been standardized and widely used in industry. Verilog programs can exhibit a rich variety of behaviours, including event-driven computation and shared-variable concurrency.

The semantics for Verilog is very important to help in ensuring the correctness of hardware design. With fellows and colleagues based at UNU/IIST, London South Bank University (LSBU), and ECNU, a series of research studies on Verilog semantics were undertaken. The operational semantics was explored by Jifeng in collaboration with Qiwen Xu, Huibiao Zhu, Jonathan Bowen, and others [13, 37, 40, 57], including the animation of Verilog’s operational semantics. Verilog’s denotational semantics [77] has also been explored based on the operational semantics using Duration Calculus [73].

Later, the linking between the denotational semantics and operational semantics for Verilog has been successfully investigated under a discrete-time model, developed by Huibiao Zhu based on Jifeng’s original ideas [74,75,76]. More recently, a mechanical approach using the Coq proof assistant tool has been applied in unifying the Verilog semantics by Feng Sheng et al. [67, 68], against developing on Jifeng’s theoretical research. The soundness and completeness of the operational semantics is verified based on the algebraic semantics via the mechanical approach in Coq. Similarly, the correctness of the algebraic laws has also been verified using a mechanical approach supported by Coq. This semantics research on Verilog semantics demonstrates the successful application of UTP in Verilog.

Advanced Features of Duration Calculus: Duration Calculus (DC) was originally proposed by Zhou Chaochen with Tony Hoare and Anders Ravn [73] as part of the ProCoS project to provide a precise formalism for requirements involving timing constraints. Several advanced features of Durational Calculus were later investigated by Jifeng in collaboration with Qiwen Xu [38], including initial and final values, stability, left and right neighbourhood values, and chopping points, aiming to integrate several variants of Duration Calculus. A link between the untimed refinement calculus and the timed one in this framework was studied, where the timed version preserves the laws of untimed programming.

rCOS: A refinement calculus of object systems (named rCOS) was studied [35, 59, 60], in collaboration with Zhiming Liu and Xiaoshan Li, defining an observation-oriented semantics for a relational object-based language with a rich variety of features including subtypes, visibility, inheritance, type casting, dynamic binding, and polymorphism. The logic of rCOS is a conservative extension of standard predicate logic. rCOS relates the notions of refinement and data refinement in imperative programming to refactorings and object-oriented design patterns for responsibility assignments. The investigation for rCOS shows the successful application of UTP in object orientation. Further more detailed information on rCOS is provided in another paper in this volume [59], including the formal use of the Unified Modeling Language (UML) [56].

4 East China Normal University

From 2002 to 2019, Jifeng He was the Dean of the Software Engineering Institute at East China Normal University in Shanghai. During this period, despite his additional administrative duties as Dean, he pioneered the theory and technology of model-based trustworthy software design. The related achievements have been widely adopted by key departments in China. Even as Dean, Jifeng continued to lead teams undertaking active research. Some notable contributions are outlined below.

Web Services: With the development of Internet technology, web services and web-based applications increasingly play an important role in information systems. Business Process Execution Language (BPEL) is used for specifying the behaviour of business processes. BPEL contains several interesting features, including scope-based compensation and fault handling. A model for BPEL-like languages and a transaction calculus have been proposed by Jifeng [29, 41]. The denotational semantics and a set of algebraic laws were also investigated. In addition, the lining of semantics for web services was also explored by Huibiao Zhu, Jifeng, and others [78,79,80].

Unification of CSP and CCS: The Calculus of Communicating Systems (CCS) of Robin Milner [61] and Communicating Sequential Processes (CSP) of Tony Hoare [42] are two major examples of the process calculi family. A process may be defined by a transition system, which is the approach taken in setting up the framework of CCS. Meanwhile, traces are the foundation of the definition of CSP. The unification of CCS and CSP was studied by Jifeng in collaboration with Tony Hoare [30, 31], and it has been proved that CSP is a retract of CCS. It is claimed that the technique of retraction is a common and useful form of unification.

HRML Language: A hybrid modelling language (HRML) [33] was proposed by Jifeng and Qin Li, with a set of novel combinators. The complex combinations of testing and reaction behaviours were conducted to model the physical world and its interaction with the control program. With the introduction of the new hybrid structures when and until, three types of guards were defined to model the condition under which the system controller switches to a new mode. A denotational semantics was studied for the HRML language using the UTP approach.

A New Roadmap for UTP: A new roadmap [34] was also proposed by Jifeng and Qin Li, for linking theories of programming, which is one of the new directions for the UTP approach. The new methodology takes an algebra of programs as its basis; it generates both denotational and operational representations from the algebraic refinement relation. A testing structure has been studied, representing the execution behaviours of programs. This new roadmap was successfully applied for the Guarded Command Language (GCL) and CSP. It is believed that this new roadmap can be applied to other types of programs with new modern features. A Coq proof assistant implementation of the program algebra in Jifeng’s UTP roadmap is included in this volume [63].

5 Conclusion

The Scopus database (https://www.scopus.com) is widely recognized as an important indicator of scientific publication record, although with a limited set of approved journals and restricted access. This orders papers by citation count. The Scopus list of top-ten academic papers coauthored by Jifeng (omitting a survey paper) are listed in Table 1. Note that Scopus has two entries for [27] separately under its main title and subtitle (which have been combined into a single entry in Table reftopten), and does not include books. For example, the UTP book [49] is probably Jifeng’s most influential work. So one should always treat such automatically generated publication statistics with caution.

Table 1. Jifeng He’s top ten most cited academic papers on the Scopus database in 2023.
Full size table

In September 2013, Jifeng’s 70th birthday was celebrated at East China Normal University with an international three-day Festschrift and an associated proceedings volume edited by Zhiming Liu, Jim Woodcock, and Huibiao Zhu [58], held in association with the International Conference on Theoretical Aspects of Computing (ICTAC). This included a paper on Jifeng’s connections within the formal methods community [3]. During this event, a poster of Jifeng was on display in a public walkway in Shanghai (see Fig. 2). The following is a translation of the statement on the poster:

He is the first [Chinese] academician in the field of computer science in Shanghai, has initiated an international school of software theory, and is acknowledged as a leader in Asian software theory. At the age of 70, he always cares about students, promotes the reform of undergraduate education and teaching, manages to organize awards and grants for students, teaches with a scientific attitude, and educates people with care.

Fig. 2.
figure 2

Poster of Jifeng He in Shanghai, 2013.

Full size image

It is interesting to try to imagine a similar public display for a computer scientist in the West.

In October 2018, Jifeng gave a presentation for the BCS-FACS (Formal Aspects of Computing Science) Specialist Group in London to celebrate the 20th anniversary of the publication of the book on UTP [49] (see Fig. 3), chaired by Jonathan Bowen (the chair of the FACS group itself). Tony Hoare, Jifeng’s coauthor, provided introductory remarks and Jim Woodcock of the University of York, a leading UTP researcher, provided a summary at the end of the talk. This event also celebrated the 30th anniversary of the Formal Aspects of Computing journal and the 40th anniversary of FACS itself [5].

Fig. 3.
figure 3

Jifeng He and Tony Hoare at the BCS-FACS event celebrating 20 years since the publication of their UTP book, held in London, 2018. (See also Fig. 1.)

Full size image

Jifeng has been a major contributor to research into formal methods during his career as a computer scientist. His collaboration with Tony Hoare, especially on the Unifying Theories of Programming, has been particularly fruitful. Tony Hoare is brilliant at initiating new ideas in computer science, but Jifeng’s contributions to UTP are equal (if not greater) in stature, as noted by Jim Woodcock [70] (page 291). Jifeng’s role has been very important in ensuring that the ideas are mathematically sound [6] and he added great insights to formulations using UTP, including for simplifying the algebraic semantics of CSP. Jifeng’s collaboration with Tony Hoare on UTP has been crucial to its success. Tony Hoare has noted [43]:

Jifeng has a long record of achievement and is enjoying the highest international regard. Jifeng has an extraordinary skill as an applied logician and was always glad to undertake the most difficult problems, and in a day or two came back with a proof or counter-example.

Commenting on their collaboration of ten year’s UTP research and the resulting book, Tony Hoare adds [43]:

I must emphasise that all the effective research was conducted by Jifeng, who formalized the definitions, postulated the axioms, and proved the theorems. I enjoyed discussing the goal of research with him, and I wrote much of the English prose. But all of the new results were due to him. Since leaving Oxford, Jifeng has successfully resolved all the main issues which were unable to put into the original book, and has developed further remarkable insights.

With this paper providing a summary of Jifeng’s lifetime of achievements, and echoing Tony Hoare’s sentiments, we thank Jifeng for furthering the foundations of computer science over his career.