Skip to content
Snippets Groups Projects
Commit 0fabfd3f authored by Peter Gerwinski's avatar Peter Gerwinski
Browse files

Vorbereitung 20.5.2025

parent 17aab801
No related branches found
No related tags found
No related merge requests found
../common/Zeichen_123.pdf
\ No newline at end of file
File added
% ad-20250520.pdf - Lecture Slides on Algorithms and Data Structures in C/C++
% Copyright (C) 2018-2024, 2025 Peter Gerwinski
%
% This document is free software: you can redistribute it and/or
% modify it either under the terms of the Creative Commons
% Attribution-ShareAlike 3.0 License, or under the terms of the
% GNU General Public License as published by the Free Software
% Foundation, either version 3 of the License, or (at your option)
% any later version.
%
% This document is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
% GNU General Public License for more details.
%
% You should have received a copy of the GNU General Public License
% along with this document. If not, see <https://www.gnu.org/licenses/>.
%
% You should have received a copy of the Creative Commons
% Attribution-ShareAlike 3.0 Unported License along with this
% document. If not, see <https://creativecommons.org/licenses/>.
% README: C++: Objekte, Strings, Templates, …
\documentclass[10pt,t]{beamer}
\usepackage{pgslides}
\usepackage{tikz}
%\usepackage{rotating}
\newcommand{\underconstruction}{%
\begin{picture}(0,0)
\color{black}
\put(6,-2.2){\makebox(0,0)[b]{\includegraphics[width=1.5cm]{Zeichen_123.pdf}}}
\put(6,-2.5){\makebox(0,0)[t]{\shortstack{Änderungen\\vorbehalten}}}
\end{picture}}
\title{Algorithmen und Datenstrukturen in C/C++}
\author{Prof.\ Dr.\ rer.\ nat.\ Peter Gerwinski}
\date{20.\ Mai 2025}
\begin{document}
\maketitleframe
\nosectionnonumber{\inserttitle}
\begin{frame}
\shownosectionnonumber
\begin{itemize}
\item[\textbf{1}] \textbf{Einführung}
\hfill\makebox(0,0)[br]{\raisebox{2.25ex}{\url{https://gitlab.cvh-server.de/pgerwinski/ad}}}
\item[\textbf{2}] \textbf{Arrays und Zeiger für Fortgeschrittene}
\item[\textbf{3}] \textbf{Langzahl-Arithmetik}
\item[\textbf{4}] \textbf{Kryptographie und Fehlerbehandlung}
\item[\textbf{5}] \textbf{Einführung in C++}
\begin{itemize}
\color{medgreen}
\item[5.0] Was ist C?
\item[5.1] Was ist C++?
% \underconstruction
\item[5.2] Elementare Neuerungen in C++ gegenüber C
\item[5.3] Referenz-Typen
\item[5.4] Überladbare Operatoren und Funktionen
\item[5.5] Namensräume
\color{orange}
\item[5.6] Objekte
\color{red}
\item[5.7] Strings
\item[5.8] Templates
\vspace{-\smallskipamount}
\item[\textbf{\dots}]
% \item[5.9] Container-Templates
% \item[5.10] Iteratoren
% \item[5.11] Exceptions
% \item[5.12] Typ-Konversionen
\end{itemize}
\item[\textbf{6}] \textbf{Datenorganisation}
\vspace{-\smallskipamount}
\item[\textbf{\dots}]
\end{itemize}
\vspace*{-1cm}
\end{frame}
\setcounter{section}{4}
\section{Einführung in C++}
\addtocounter{subsection}{-1}
\subsection{Was ist C?}
\begin{frame}
\showsection
\showsubsection
Etabliertes Profi-Werkzeug
\begin{itemize}
\item
kleinster gemeinsamer Nenner für viele Plattformen\\
\begin{picture}(0,1)
\color{red}
\put(7.2,0.6){\tikz{\draw[-latex](0.0,0.0)--(0.0,0.4);}}
\put(7.2,0.5){\makebox(0,0)[t]{\color{black}Hardware und/oder Betriebssystem}}
\end{picture}
\item
Hardware direkt ansprechen und effizient einsetzen
\item
\dots\ bis hin zu komplexen Software-Projekten
\medskip
\arrowitem
Man kann Computer vollständig beherrschen.
\end{itemize}
\end{frame}
\begin{frame}
\showsection
\showsubsection
\begin{picture}(0,0)
\put(5.3,-2.5){\makebox(0,0)[tl]{\begin{minipage}{7cm}
\emph{C makes it easy to shoot yourself in the foot.}
\begin{flushright}
Bjarne Stroustrup, ca.~1986\\
\href{https://www.stroustrup.com/bs_faq.html\#really-say-that}%
{\nolinkurl{https://www.stroustrup.com/bs_faq.html}\\
\nolinkurl{\#really-say-that}}
\end{flushright}
\end{minipage}}}
\end{picture}%
Etabliertes Profi-Werkzeug
\begin{itemize}
\item
kleinster gemeinsamer Nenner für viele Plattformen
\item
Hardware direkt ansprechen und effizient einsetzen
\item
\dots\ bis hin zu komplexen Software-Projekten
\item
leistungsfähig, aber gefährlich
\end{itemize}
\medskip
"`High-Level-Assembler"'
\begin{itemize}
\item
kein "`Fallschirm"'
\item
kompakte Schreibweise
\end{itemize}
\medskip
Unix-Hintergrund
\begin{itemize}
\item
Baukastenprinzip
\item
konsequente Regeln
\item
kein "`Fallschirm"'
\end{itemize}
\end{frame}
\subsection{Was ist C++?}
\begin{frame}
\showsection
\showsubsection
\begin{picture}(0,0)
\put(6.3,-0.2){\makebox(0,0)[tl]{\begin{minipage}{6cm}
\emph{C++ is a better C.}
\begin{flushright}
Bjarne Stroustrup, Autor von C++\\
\url{https://www.stroustrup.com/C++.html}
\end{flushright}
\end{minipage}}}
\put(5.3,-2.5){\makebox(0,0)[tl]{\begin{minipage}{7cm}
\emph{C makes it easy to shoot yourself in the foot;\\
C++ makes it harder, but when you do\\
it blows your whole leg off.}
\begin{flushright}
Bjarne Stroustrup, Autor von C++, ca.~1986\\
\href{https://www.stroustrup.com/bs_faq.html\#really-say-that}%
{\nolinkurl{https://www.stroustrup.com/bs_faq.html}\\
\nolinkurl{\#really-say-that}}
\end{flushright}
\end{minipage}}}
\end{picture}%
Etabliertes Profi-Werkzeug
\begin{itemize}
\item
kompatibel zu C
\end{itemize}
\medskip
C++ unterstützt
\begin{itemize}
\item
\newterm{objektorientierte\\
Programmierung}
\item
\newterm{Datenabstraktion}
\item
\newterm{generische\\
Programmierung}
\end{itemize}
\vspace{0cm plus 1 filll}
\textbf{Motivation:}\\[\smallskipamount]
Vermeidung unsicherer Techniken,\\
insbesondere von Präprozessor-Konstruktionen und Zeigern,\\
unter Beibehaltung der Effizienz
\end{frame}
\subsection{Elementare Neuerungen in C++ gegenüber C}
\begin{frame}[fragile]
\showsubsection
\begin{itemize}
% \pause
\item
Kommentare mit \lstinline{//}
% \pause
\item
Konstante:
\begin{onlyenv}<3>
\begin{lstlisting}[gobble=10]
const int answer = 42;
\end{lstlisting}
\end{onlyenv}
\begin{lstlisting}[gobble=8]
const int n = 5;
int prime[n] = { 2, 3, 5, 7, 11 };
\end{lstlisting}
% \pause
\item
Ab C++11: \lstinline{constexpr}-Funktionen\\
% \only<1->{{\color{red}\dots\ anscheinend auch ohne "`constexpr"' \dots}\\}
C++11: darf nur aus einem einzigen \lstinline{return}-Statement bestehen\\
\textarrow\ \lstinline{?:} statt \lstinline{if}, Rekursion statt Schleife\\
C++-14: auch Verzweigungen und Schleifen erlaubt
% \pause
\item
leere Parameterliste: \lstinline{void} optional\\
in C: ohne \lstinline{void} = Parameterliste wird nicht geprüft
% \pause
\item
Operatoren \lstinline{new} und \lstinline{delete}\\
als Alternative zu den Funktionen \lstinline{malloc()} und \lstinline{free()}
\end{itemize}
\end{frame}
\subsection{Referenz-Typen}
\begin{frame}[fragile]
\showsubsection
\begin{lstlisting}
void calc_answer (int &answer)
{
answer = 42;
}
\end{lstlisting}
\medskip
\dots\ als Alternative zu \dots
\medskip
\begin{lstlisting}
void calc_answer (int *answer)
{
*answer = 42;
}
\end{lstlisting}
\begin{itemize}
\item
Zeiger "`verborgen"', übersichtlicher und sicherer
\item
Es gibt keinen \lstinline{NULL}-Wert.\\
\textarrow\ Für verkettete Listen u.\,ä.: Tricks erforderlich
\end{itemize}
\end{frame}
\subsection{Überladbare Operatoren und Funktionen}
\begin{frame}[fragile]
\showsubsection
\begin{lstlisting}
#include <iostream>
int main ()
{
std::cout << "Hello, world!" << std::endl;
return 0;
}
\end{lstlisting}
% \pause
\bigskip
Bemerkungen:
\begin{itemize}
\item
Compilieren mit \lstinline[style=cmd]{g++}
statt \lstinline[style=cmd]{gcc}:\\
C++-Bibliotheken mit einbinden
\item
Der Operator \lstinline{<<} hat normalerweise keinen Seiteneffekt,
hier schon.
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\showsubsection
\begin{lstlisting}
#include <iostream>
struct vector
{
double x, y, z;
};
vector operator + (vector u, vector v)
{
vector w = { u.x + v.x, u.y + v.y, u.z + v.z };
return w;
}
\end{lstlisting}
\begin{itemize}
\item
\lstinline{++} wird zum Präfix-Operator.
\item
\lstinline{++} mit zusätzlichem (ungenutzten) \lstinline{int}-Parameter\\
wird zum Postfix-Operator.
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\showsubsection
\begin{lstlisting}
void print (const char *s)
{
printf ("%s", s);
}
void print (int i)
{
printf ("%d", i);
}
\end{lstlisting}
% \pause
\bigskip
Optionale Parameter:
\medskip
\begin{lstlisting}
void print (const char *s = "\n")
{
printf ("%s", s);
}
\end{lstlisting}
% \pause
\begin{picture}(0,0)
\color{red}
\put(5.50,5.40){\makebox(0,0)[br]{\tikz{\draw[-latex](0.0,0.0)--(-2.0,0.6);}}}
\put(5.50,4.85){\makebox(0,0)[tr]{\tikz{\draw[-latex](0.0,0.0)--(-2.0,-0.2);}}}
\put(5.6,5.0){\begin{minipage}{5cm}
Für den Linker:\\
veränderte, eindeutige Namen
\end{minipage}}
\put(5.50,1.55){\makebox(0,0)[tr]{\tikz{\draw[-latex](0.0,0.0)--(-0.6,0.4);}}}
\put(5.6,1.0){\begin{minipage}{5cm}
wird vom Compiler erledigt
\end{minipage}}
% \pause
\put(7.0,3.6){\makebox(0,0)[b]{\tikz{\draw[-latex](0.0,0.0)--(0.0,0.9);}}}
\put(5.6,3.0){\begin{minipage}{5cm}
Wenn man das nicht will:\\
extern \char`"C\char`"\ \{ \dots \}
\end{minipage}}
\end{picture}
\end{frame}
\subsection{Namensräume}
\begin{frame}[fragile]
\showsubsection
\begin{lstlisting}
#include <iostream>
using namespace std;
int main ()
{
cout << "Hello, world!" << endl;
return 0;
}
\end{lstlisting}
% \pause
\bigskip
\begin{lstlisting}
namespace my_output
{
...
}
using namespace my_output;
\end{lstlisting}
\end{frame}
\subsection{Objekte}
\begin{frame}[fragile]
\showsubsection
\begin{center}
\begin{minipage}{5cm}
\begin{lstlisting}[gobble=8]
¡struct TBase
{
};¿
\end{lstlisting}
\end{minipage}\\[0.5cm]
\begin{minipage}{6cm}
\begin{lstlisting}[gobble=8]
¡struct TInteger: public TBase
{
int content;
};¿
\end{lstlisting}
\end{minipage}
\begin{minipage}{5cm}
\begin{lstlisting}[gobble=8]
¡struct TString: public TBase
{
char *content;
};¿
\end{lstlisting}
\end{minipage}
\end{center}
\end{frame}
\subsubsection{Zugriffsrechte}
\begin{frame}[fragile]
\showsubsection
\showsubsubsection
\begin{itemize}
\item
\lstinline{public}, \lstinline{private}, \lstinline{protected}\\[\smallskipamount]
nicht nur Bürokratie, sondern auch Kapselung\\
(Maßnahme gegen "`Namensraumverschmutzung"')
\medskip
\item
\lstinline{struct}: standardmäßig \lstinline{public}\\[\smallskipamount]
\lstinline{class}: standardmäßig \lstinline{private}
\medskip
\item
\lstinline{friend}-Funktionen und -Klassen
\medskip
\item
Klasse als Namensraum:\\
\lstinline{static}-"`Member"'-Variable\\
\lstinline{static}-"`Methoden"'\\
Deklarationen von z.\,B.\ Konstanten und Typen
\end{itemize}
\end{frame}
\subsubsection{Konstruktoren und Destruktoren}
\begin{frame}[fragile]
\showsubsection
\showsubsubsection
\begin{itemize}
\item
leerer Standard-Konstrutor
\item
\newterm{Copy-Konstruktor}
\item
Konstruktor-Aufruf als "`Initialisierung"'
\item
Konstruktor-Aufruf mit \lstinline{new}\\
Destruktor-Aufruf mit \lstinline{delete}
\item
automatischer Destruktor-Aufruf\\
beim Verlassen des Gültigkeitsbereichs
\end{itemize}
\end{frame}
\subsection{Strings}
\begin{frame}[fragile]
\showsubsection
\begin{itemize}
\item
\lstinline{#include <string>}
\item
String-Klasse
\item
String-Konstante sind \lstinline{const char *}
\item
C-kompatiblen String extrahieren: \lstinline{c_str ()}
\item
In String schreiben: \lstinline{#include <sstream>}, \lstinline{ostringstream}
\end{itemize}
\end{frame}
\subsection{Templates}
\begin{frame}[fragile]
\showsubsection
Anwendung desselben Quelltextes auf verschiedene Datentypen
\begin{itemize}
\item
\lstinline{template <typename x> ...}
\item
\lstinline{template <class x> ...}
\end{itemize}
\pause
Vorsicht: Fehler werden erst bei Instantiierung erkannt!
\pause
\begin{itemize}
\item
Template-Spezialisierung:\\
\lstinline{template <> foo <int> ...}
\end{itemize}
\end{frame}
\subsection{Container-Templates}
\begin{frame}
% \showsection
\showsubsection
\vspace*{-0.25cm}
\begin{tabular}{ll}
\lstinline|array| & Array mit fester Größe \\
\lstinline|bitset| & festes Array von Bits (Booleans) \\
\lstinline|vector| & dynamisches Array \\
\lstinline|vector <bool>| & dynamisches Bit-Array \\
\lstinline|forward_list| & einfach-verkettete Liste \\
\lstinline|list| & doppelt-verkettete Liste \\
\lstinline|set| & binärer Baum \\
\lstinline|multiset| & mehrfache Elemente zulässig \\
\lstinline|unordered_set| & Hash-Tabelle \\
\lstinline|unordered_multiset| & mehrfache Elemente zulässig \\
\lstinline|map| & binärer Baum mit separaten Schlüsselwerten \\
\lstinline|multimap| & mehrere Elemente pro Schlüssel \\
\lstinline|unordered_map| & Hash-Tabelle mit separaten Schlüsselwerten \\
\lstinline|unordered_multimap| & mehrere Elemente pro Schlüssel \\
\lstinline|stack| & Stack \\
\lstinline|queue| & FIFO \\
\lstinline|deque| & \emph{\textbf{d}ouble-\textbf{e}nded \textbf{que}ue} \\
\lstinline|priority_queue| & geordneter Push-Pop-Container
\end{tabular}\\[3pt]
\url{https://cplusplus.com/reference/stl/}
\vspace*{-1cm}
\end{frame}
\subsection{Iteratoren}
\begin{frame}[fragile]
% \showsection
\showsubsection
Pointer-Arithmetik:
\medskip
\begin{lstlisting}
int prime[5] = { 2, 3, 5, 7, 11 };
for (int *p = prime; p != prime + 5; p++)
std::cout << *p << std::endl;
\end{lstlisting}
\bigskip
Iterator als Verallgemeinerung:
\medskip
\begin{lstlisting}
std::array <int, 5> prime = { { 2, 3, 5, 7, 11 } };
for (std::array <int, 5>::iterator p = prime.begin (); p != prime.end (); p++)
std::cout << *p << std::endl;
\end{lstlisting}
\end{frame}
\subsection{Exceptions}
\begin{frame}[fragile]
\showsubsection
\begin{lstlisting}
try
{
...
throw <value>;
...
}
catch (<type> <variable>)
{
...
}
catch ...
\end{lstlisting}
\vspace*{-4.6cm}\hspace*{5cm}
\begin{minipage}{7cm}
\begin{itemize}
\item
Nach den \lstinline{catch()}-Statements wird,
soweit nicht anders programmiert, das Programm fortgesetzt.
\medskip
\item
\lstinline{throw;} (ohne Wert):\\
an übergeordneten Exception-Handler weiterreichen
\medskip
\item
C-Äquivalent:\\
\lstinline{setjmp()}, \lstinline{longjmp()}
\medskip
\item
speziell für \lstinline{<type>}:\\
Nachfahren von \lstinline{class exception}
\medskip
\item
veraltet:\\
\newterm{dynamic exception specifications}
\end{itemize}
\end{minipage}
\end{frame}
\subsection{Typ-Konversionen}
\begin{frame}[fragile]
\showsubsection
\begin{itemize}
\item
In C:
\begin{lstlisting}[gobble=8]
char *hello = "Hello, world!";
uint64_t address = (uint64_t) hello;
printf ("%" PRIu64 "\n", address);
\end{lstlisting}
\smallskip
\item
alternative Syntax in C++:
\begin{lstlisting}[gobble=8]
char *hello = "Hello, world!";
uint64_t address = uint64_t (hello);
cout << address << endl;
\end{lstlisting}
\smallskip
\item
zusätzlich in C++:\\
implizite und explizite Typumwandlung zwischen Zeigern auf Klassen\\
\lstinline{dynamic_cast<>()}\\
\lstinline{static_cast<>()}\\
\lstinline{reinterpret_cast<>()}\\
\lstinline{const_cast<>()}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\showsubsection
\url{https://www.cplusplus.com/doc/tutorial/typecasting/}
\begin{itemize}
\item
Zuweisung: Zeiger auf abgeleitete Klasse an Zeiger auf Basisklasse\\
\textarrow\ implizite Typumwandlung möglich
\smallskip
\item
Zuweisung: Zeiger auf Basisklasse an Zeiger auf abgeleitete Klasse\\
\textarrow\ nur explizite Typumwandlung möglich:\\
\hspace*{0.76cm}\lstinline{dynamic_cast<>()}, \lstinline{static_cast<>()}
\smallskip
\item
implizite Typumwandlungen in der Klasse definieren:
\begin{itemize}
\item
Initialisierung durch Konstruktor
\item
Zuweisungs-Operator
\item
Typumwandlungsoperator
\end{itemize}
\smallskip
\item
implizite Typumwandlungen ausschalten:\\
Schlüsselwort \lstinline{explicit}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\showsubsection
\url{https://www.cplusplus.com/doc/tutorial/typecasting/}
\begin{itemize}
\item
\lstinline{dynamic_cast<>()}\\
Zuweisung: Zeiger auf Basisklasse an Zeiger auf abgeleitete Klasse\\
explizite Typumwandlung mit Prüfung, ggf.\ Exception
\smallskip
\item
\lstinline{static_cast<>()}\\
Zuweisung: Zeiger auf Basisklasse an Zeiger auf abgeleitete Klasse\\
explizite Typumwandlung ohne Prüfung
\smallskip
\item
\lstinline{reinterpret_cast<>()}\\
Typumwandlung ohne Prüfung zwischen Zeigern untereinander\\
und zwischen Zeigern und Integer-Typen
\smallskip
\item
\lstinline{const_cast<>()}\\
"`\lstinline{const}"' ein- bzw.\ ausschalten
\end{itemize}
\end{frame}
\end{document}
../common/logo-hochschule-bochum-cvh-text-v3.pdf
\ No newline at end of file
../common/logo-hochschule-bochum-de-narrow.pdf
\ No newline at end of file
../common/pgslides.sty
\ No newline at end of file
...@@ -23,6 +23,7 @@ Vortragsfolien und Beispiele: ...@@ -23,6 +23,7 @@ Vortragsfolien und Beispiele:
* [29.04.2025: Quaternionen, Diffie-Hellman, ElGamal](https://gitlab.cvh-server.de/pgerwinski/ad/raw/2025ss/20250429/ad-20250429.pdf) [**(Beispiele)**](https://gitlab.cvh-server.de/pgerwinski/ad/tree/2025ss/20250429/) * [29.04.2025: Quaternionen, Diffie-Hellman, ElGamal](https://gitlab.cvh-server.de/pgerwinski/ad/raw/2025ss/20250429/ad-20250429.pdf) [**(Beispiele)**](https://gitlab.cvh-server.de/pgerwinski/ad/tree/2025ss/20250429/)
* [06.05.2025: Parität, CRC, Hadamard-Code, RAID](https://gitlab.cvh-server.de/pgerwinski/ad/raw/2025ss/20250506/ad-20250506.pdf) [**(Beispiele)**](https://gitlab.cvh-server.de/pgerwinski/ad/tree/2025ss/20250506/) * [06.05.2025: Parität, CRC, Hadamard-Code, RAID](https://gitlab.cvh-server.de/pgerwinski/ad/raw/2025ss/20250506/ad-20250506.pdf) [**(Beispiele)**](https://gitlab.cvh-server.de/pgerwinski/ad/tree/2025ss/20250506/)
* [13.05.2025: Einführung in C++](https://gitlab.cvh-server.de/pgerwinski/ad/raw/2025ss/20250513/ad-20250513.pdf) [**(Beispiele)**](https://gitlab.cvh-server.de/pgerwinski/ad/tree/2025ss/20250513/) * [13.05.2025: Einführung in C++](https://gitlab.cvh-server.de/pgerwinski/ad/raw/2025ss/20250513/ad-20250513.pdf) [**(Beispiele)**](https://gitlab.cvh-server.de/pgerwinski/ad/tree/2025ss/20250513/)
* [20.05.2025: C++: Objekte, Strings, Templates, …](https://gitlab.cvh-server.de/pgerwinski/ad/raw/2025ss/20250520/ad-20250520.pdf) [**(Beispiele)**](https://gitlab.cvh-server.de/pgerwinski/ad/tree/2025ss/20250520/)
* [alle in 1 Datei](https://gitlab.cvh-server.de/pgerwinski/ad/raw/2025ss/ad-slides-2025ss.pdf) * [alle in 1 Datei](https://gitlab.cvh-server.de/pgerwinski/ad/raw/2025ss/ad-slides-2025ss.pdf)
Tafelbilder: Tafelbilder:
......
No preview for this file type
...@@ -22,4 +22,6 @@ ...@@ -22,4 +22,6 @@
\includepdf[pages=-]{20250506/ad-20250506.pdf} \includepdf[pages=-]{20250506/ad-20250506.pdf}
\pdfbookmark[1]{13.05.2025: Einführung in C++}{20250513} \pdfbookmark[1]{13.05.2025: Einführung in C++}{20250513}
\includepdf[pages=-]{20250513/ad-20250513.pdf} \includepdf[pages=-]{20250513/ad-20250513.pdf}
\pdfbookmark[1]{20.05.2025: C++: Objekte}{20250520}
\includepdf[pages=-]{20250520/ad-20250520.pdf}
\end{document} \end{document}
Geplante Projekte:
* Passwort-Manager in Rust
* Frontend zur Live-Anzeige von Wahlergebnissen
* Objekterkennung: OpenCV verstehen
Projektideen:
* https://gitlab.cvh-server.de/hardwarenahe-it/projekte
* Freies Smartphone
* Wayland für PG
* Mathematik-Programm: Proof Assistant
Challenges with Lean 4
- steep learning curve
- precision: You have to spell out everything. There is no "trivial".
- complexity
- limited libraries
- documentation
- searchability
The iPhone-moment for Lean 4 is still to come.
"It's still work [to start with it]. But it's fun."
Example:
theorem prime_infinite : ... by
intro n
have : 2 <= Nat.factorial (n + 1) + 1 := by
sorry
cases ...
* Rechnungen zur Allgemeinen Relativitätstheorie
Bibliothek: Cactus
Mögliche Rechnung: Kollision zweier schwarzer Löcher
Ziel: Bibliothek verstehen und Benutzung dokumentieren
Hintergrundwissen: ggf. Prof. Gerwinski fragen
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment