Not quite.

The books you mention deal with "Software Abstractions" i.e. Procedural Abstraction, Data Abstraction, ADT, Patterns etc. They are at a much higher level than Dijkstra's concepts.

What Dijkstra is talking about is the Set Theory/Logic Operations underlying all of them. This is why he was sceptical of OO/Functional etc. styles of programming. They were all mere syntactic sugar over the underlying Mathematics obscuring the essence of Programming. For him all computation is basically a series of manipulating values from a Set as a whole using Logical Expressions i.e. Predicate Calculus.

Again from EWD1036;

Before we part, I would like to invite you to consider the following way of doing justice to computing's radical novelty in an introductory programming course.

On the one hand, we teach what looks like the predicate calculus, but we do it very differently from the philosophers. In order to train the novice programmer in the manipulation of uninterpreted formulae, we teach it more as boolean algebra, familiarizing the student with all algebraic properties of the logical connectives. To further sever the links to intuition, we rename the values {true, false} of the boolean domain as {black, white}.

On the other hand, we teach a simple, clean, imperative programming language, with a skip and a multiple assignment as basic statements, with a block structure for local variables, the semicolon as operator for statement composition, a nice alternative construct, a nice repetition and, if so desired, a procedure call. To this we add a minimum of data types, say booleans, integers, characters and strings. The essential thing is that, for whatever we introduce, the corresponding semantics is defined by the proof rules that go with it.

Right from the beginning, and all through the course, we stress that the programmer's task is not just to write down a program, but that his main task is to give a formal proof that the program he proposes meets the equally formal functional specification. While designing proofs and programs hand in hand, the student gets ample opportunity to perfect his manipulative agility with the predicate calculus. Finally, in order to drive home the message that this introductory programming course is primarily a course in formal mathematics, we see to it that the programming language in question has not been implemented on campus so that students are protected from the temptation to test their programs. And this concludes the sketch of my proposal for an introductory programming course for freshmen.

The language mentioned above is described in EWD472 (also see wikipedia for a detailed explanation - https://en.wikipedia.org/wiki/Guarded_Command_Language). Notice the total absence of syntactic sugar and fancy computation models i.e. no complex Types, no mapping to lambda calculus or any other mathematical model (since a computer is fundamentally imperative over a state space) etc. It is just the absolute basic mathematics of Set Theory and Logic.

Note that Tony Hoare had systematized the algebra for this in his "Hoare Logic" via Pre/Post conditions for a executable statement - https://en.wikipedia.org/wiki/Hoare_logic

Dijsktra then went one-step further by giving automatic calculational rules to derive a program by simple logical manipulation of symbols. In this case we reason backwards from the output of the program (known apriori from its functional specification) i.e. from postcondition to precondition using the idea of a predicate transformer. This is his weakest-precondition (wp) calculus where with each executable program statement a Pre = wp(Statement, Post) total function is defined by the Programmer i.e. his code must satisfy the function which is the predicate transformer transforming the postcondition to a weakest-preconditon. See this wikipedia page on Predicate Transformer Semantics for a nice detailed explanation - https://en.wikipedia.org/wiki/Predicate_transformer_semantic...